α : Type ?u.21876
r : α → α → Prop
ι : Type u
f : ι → Ordinal
⊢ sInf {a | ∃ ι_1 f_1, lsub f_1 = lsub f ∧ (#ι_1) = a} ≤ (#ι)
α : Type ?u.21876
r : α → α → Prop
ι : Type u
f : ι → Ordinal
⊢ cof (lsub f) ≤ (#ι)
rw [cof_eq_sInf_lsub]
no goals
α : Type ?u.21876
r : α → α → Prop
ι : Type u
f : ι → Ordinal
⊢ sInf {a | ∃ ι_1 f_1, lsub f_1 = lsub f ∧ (#ι_1) = a} ≤ (#ι)
exact csInf_le' ⟨ι, f, rfl, rfl⟩