def definition def or abbrev

`OverlapLowerBoundOS`

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

formal statement (Lean)

  39def OverlapLowerBoundOS (_K : Kernel) (β : ℝ) : Prop := 0 < β ∧ β ≤ 1

Definition body.

  40
  41/-- Perron–Frobenius transfer spectral gap property. -/

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

Lean names referenced from this declaration's body.