α : Type ?u.39412
r : α → α → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ cof (blsub o f) ≤ Cardinal.lift (card o)
α : Type ?u.39412
r : α → α → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ cof (blsub o f) ≤ card o
rw [← o.card.lift_id]
no goals
α : Type ?u.39412
r : α → α → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ cof (blsub o f) ≤ Cardinal.lift (card o)
exact cof_blsub_le_lift f