theorem proved term proof

`rotational_flatness_implies_nonzero_vflat`

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

formal statement (Lean)

  45theorem rotational_flatness_implies_nonzero_vflat (P : Params) (r : ℝ)
  46    (hα : P.alpha > 0) :
  47    ∃ v_flat : ℝ, v_flat ≠ 0 := by

proof body

Term-mode proof.

  48  rcases rotational_flatness_implies_positive_vflat P r hα with ⟨v_flat, hv⟩
  49  exact ⟨v_flat, ne_of_gt hv⟩
  50
  51end ILG
  52end IndisputableMonolith.Gravity

depends on (6)

Lean names referenced from this declaration's body.

alpha in IndisputableMonolith.Constants.Alpha decl_use
Params in IndisputableMonolith.Gravity.ILG decl_use
rotational_flatness_implies_positive_vflat in IndisputableMonolith.Gravity.ILGDerivation decl_use
Params in IndisputableMonolith.ILG.Params decl_use
Params in IndisputableMonolith.Relativity.ILG.Params decl_use
Params in IndisputableMonolith.Spiral.SpiralField decl_use