pith. machine review for the scientific record. sign in
theorem proved wrapper

m_b_predicted_pos

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  47theorem m_b_predicted_pos (alpha_at_mb alpha_at_MZ : ℝ)
  48    (h_alpha_pos : 0 < alpha_at_mb) (h_alpha_0_pos : 0 < alpha_at_MZ) :
  49    0 < m_b_predicted alpha_at_mb alpha_at_MZ :=

proof body

One-line wrapper that applies m_running_pos.

  50  m_running_pos _ _ _ 5 m_b_at_MZ_pos h_alpha_pos h_alpha_0_pos
  51

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.