α : Type ?u.356399
β : Type ?u.356402
γ : Type ?u.356405
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
h : bsup o f = blsub o f
i : Ordinal
⊢ ∀ (hi : i < o), f i hi < blsub o f
α : Type ?u.356399
β : Type ?u.356402
γ : Type ?u.356405
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
h : bsup o f = blsub o f
i : Ordinal
⊢ ∀ (hi : i < o), f i hi < bsup o f
rw [h]
no goals
α : Type ?u.356399
β : Type ?u.356402
γ : Type ?u.356405
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
h : bsup o f = blsub o f
i : Ordinal
⊢ ∀ (hi : i < o), f i hi < blsub o f
apply lt_blsub