α : Type ?u.41243
r : α → α → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ (∀ (i : Ordinal) (h : i < o), f i h < bsup o f) → cof (bsup o f) ≤ Cardinal.lift (card o)
α : Type ?u.41243
r : α → α → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ (∀ (i : Ordinal) (h : i < o), f i h < bsup o f) → cof (bsup o f) ≤ card o
rw [← o.card.lift_id]
no goals
α : Type ?u.41243
r : α → α → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ (∀ (i : Ordinal) (h : i < o), f i h < bsup o f) → cof (bsup o f) ≤ Cardinal.lift (card o)
exact cof_bsup_le_lift