Mathlib Map

Theorems · Theorem · logic and foundations

Ordinal.iSup_add_one_le_iff

∀ {ι : Type u_3} {f : ι → Ordinal.{u}} {a : Ordinal.{u}} [Small.{u, u_3} ι], ⨆ i, f i + 1 ≤ a ↔ ∀ (i : ι), f i < a
Defined in
Mathlib.SetTheory.Ordinal.Family
Cited by
1 results in Mathlib
Foundations
Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
Small
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Ordinal.lsub_le_iff · cited by 6Ordinal.lsub_le_iffiSup · cited by 2415iSupOrdinal · cited by 1688OrdinalSmall · cited by 369SmallOrdinal.iSup_add_one_le_iffCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • iSupstatement · cited by 2,415
  • Ordinalstatement and proof · cited by 1,688
  • Smallstatement and proof · cited by 369

Cited by1

Results whose statement or proof uses this declaration.