Theorems · Theorem · logic and foundations

Ordinal.nfpFamily_lt_ord_lift

∀ {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v}} {c : Ordinal.{max u v}},
  Cardinal.aleph0 < c.cof →
    Cardinal.lift.{v, u} (Cardinal.mk ι) < c.cof →
      (∀ (i : ι), ∀ b < c, f i b < c) → ∀ {a : Ordinal.{max u v}}, a < c → Ordinal.nfpFamily f a < c

Defined in

Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Cited by

4 results in Mathlib

Foundations

Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound