def definition def or abbrev

`MassGapCont`

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

formal statement (Lean)

  51def MassGapCont (γ : ℝ) : Prop := ∃ μ : LatticeMeasure, MassGap μ γ ∧ GapPersists γ

Definition body.

  52
  53/-- OS positivity + PF transfer gap yields a lattice mass gap. -/

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

Lean names referenced from this declaration's body.