`rotational_flatness_implies_nonzero_vflat`

proved

show as: view math explainer →

module: IndisputableMonolith.Gravity.ILGDerivation
domain: Gravity
line: 45 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Gravity.ILGDerivation on GitHub at line 45.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  42  exact ⟨v_flat, hv⟩
  43
  44/-- Rotational-flatness structure excludes a zero asymptotic velocity scale. -/
  45theorem rotational_flatness_implies_nonzero_vflat (P : Params) (r : ℝ)
  46    (hα : P.alpha > 0) :
  47    ∃ v_flat : ℝ, v_flat ≠ 0 := by
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.