theorem
proved
term proof
mass_gap_continuum
show as:
view Lean formalization →
formal statement (Lean)
59theorem mass_gap_continuum {μ : LatticeMeasure} {γ : ℝ}
60 (hGap : MassGap μ γ) (hPers : GapPersists γ) : MassGapCont γ := by
proof body
Term-mode proof.
61 exact ⟨μ, hGap, hPers⟩
62
63end
64end OS
65end YM
66end IndisputableMonolith