α : Type ?u.40854
r : α → α → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
H : (bsup o fun i h => f i h) = blsub o fun i h => f i h
⊢ cof (bsup o f) ≤ Cardinal.lift (card o)
α : Type ?u.40854
r : α → α → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
H : ∀ (i : Ordinal) (h : i < o), f i h < bsup o f
⊢ cof (bsup o f) ≤ Cardinal.lift (card o)
rw [← bsup_eq_blsub_iff_lt_bsup.{u, v}] at H
α : Type ?u.40854
r : α → α → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
H : (bsup o fun i h => f i h) = blsub o fun i h => f i h
⊢ cof (blsub o fun i h => f i h) ≤ Cardinal.lift (card o)
α : Type ?u.40854
r : α → α → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
H : (bsup o fun i h => f i h) = blsub o fun i h => f i h
⊢ cof (bsup o f) ≤ Cardinal.lift (card o)
rw [H]
no goals
α : Type ?u.40854
r : α → α → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
H : (bsup o fun i h => f i h) = blsub o fun i h => f i h
⊢ cof (blsub o fun i h => f i h) ≤ Cardinal.lift (card o)
exact cof_blsub_le_lift.{u, v} f