Theorems · Theorem · logic and foundations

Cardinal.mk_biUnion_le_of_le_lift

∀ {β : Type v} {o : Ordinal.{u}} {c : Cardinal.{v}},
  Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c →
    Cardinal.aleph0 ≤ c →
      ∀ (A : Ordinal.{u} → Set β), (∀ j < o, Cardinal.mk ↑(A j) ≤ c) → Cardinal.mk ↑(⋃ j, ⋃ (_ : j < o), A j) ≤ c

Bounds the cardinal of an ordinal-indexed union of sets.

Defined in

Mathlib.SetTheory.Cardinal.Ordinal

Cited by

3 results in Mathlib

Foundations

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