α : Type ?u.366269
β : Type ?u.366272
γ : Type ?u.366275
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
H : IsNormal f
o : Ordinal
h : IsLimit o
⊢ ∀ (a : Ordinal), a < o → f a < f (succ a)
α : Type ?u.366269
β : Type ?u.366272
γ : Type ?u.366275
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
H : IsNormal f
o : Ordinal
h : IsLimit o
⊢ (blsub o fun x x_1 => f x) = f o
rw [← IsNormal.bsup_eq.{u, v} H h, bsup_eq_blsub_of_lt_succ_limit h]
no goals
α : Type ?u.366269
β : Type ?u.366272
γ : Type ?u.366275
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
H : IsNormal f
o : Ordinal
h : IsLimit o
⊢ ∀ (a : Ordinal), a < o → f a < f (succ a)
exact fun a _ => H.1 a