α : Type ?u.21105
r : α → α → Prop
o : Ordinal
⊢ sInf {a | ∃ ι f, lsub f = o ∧ (#ι) = a} ≤ card o
α : Type ?u.21105
r : α → α → Prop
o : Ordinal
⊢ cof o ≤ card o
rw [cof_eq_sInf_lsub]
no goals
α : Type ?u.21105
r : α → α → Prop
o : Ordinal
⊢ sInf {a | ∃ ι f, lsub f = o ∧ (#ι) = a} ≤ card o
exact csInf_le' card_mem_cof