α : Type ?u.356828
β : Type ?u.356831
γ : Type ?u.356834
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
ho : IsLimit o
f : (a : Ordinal) → a < o → Ordinal
hf : ∀ (a : Ordinal) (ha : a < o), f a ha < f (succ a) (_ : succ a < o)
⊢ ∀ (i : Ordinal) (hi : i < o), f i hi < bsup o f
α : Type ?u.356828
β : Type ?u.356831
γ : Type ?u.356834
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
ho : IsLimit o
f : (a : Ordinal) → a < o → Ordinal
hf : ∀ (a : Ordinal) (ha : a < o), f a ha < f (succ a) (_ : succ a < o)
⊢ bsup o f = blsub o f
rw [bsup_eq_blsub_iff_lt_bsup]
no goals
α : Type ?u.356828
β : Type ?u.356831
γ : Type ?u.356834
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
ho : IsLimit o
f : (a : Ordinal) → a < o → Ordinal
hf : ∀ (a : Ordinal) (ha : a < o), f a ha < f (succ a) (_ : succ a < o)
⊢ ∀ (i : Ordinal) (hi : i < o), f i hi < bsup o f
exact fun i hi => (hf i hi).trans_le (le_bsup f _ _)