o : Ordinal
ho : Ordinal.IsLimit o
⊢ aleph' o ≤ ⨆ (a : ↑(Iio o)), aleph' ↑a
o : Ordinal
ho : Ordinal.IsLimit o
⊢ aleph' o = ⨆ (a : ↑(Iio o)), aleph' ↑a
refine' le_antisymm _ (ciSup_le' fun i => aleph'_le.2 (le_of_lt i.2))
o : Ordinal
ho : Ordinal.IsLimit o
⊢ ∀ (o' : Ordinal), o' < o → aleph' o' ≤ ⨆ (a : ↑(Iio o)), aleph' ↑a
o : Ordinal
ho : Ordinal.IsLimit o
⊢ aleph' o ≤ ⨆ (a : ↑(Iio o)), aleph' ↑a
rw [aleph'_le_of_limit ho]
no goals
o : Ordinal
ho : Ordinal.IsLimit o
⊢ ∀ (o' : Ordinal), o' < o → aleph' o' ≤ ⨆ (a : ↑(Iio o)), aleph' ↑a
exact fun a ha => le_ciSup (bddAbove_of_small _) (⟨a, ha⟩ : Iio o)