α : Type ?u.366416
β : Type ?u.366419
γ : Type ?u.366422
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
x✝ : (∀ (a : Ordinal), f a < f (succ a)) ∧ ∀ (o : Ordinal), IsLimit o → (bsup o fun x x_1 => f x) = f o
h₁ : ∀ (a : Ordinal), f a < f (succ a)
h₂ : ∀ (o : Ordinal), IsLimit o → (bsup o fun x x_1 => f x) = f o
o : Ordinal
ho : IsLimit o
a : Ordinal
⊢ (bsup o fun x x_1 => f x) ≤ a ↔ ∀ (b : Ordinal), b < o → f b ≤ a
α : Type ?u.366416
β : Type ?u.366419
γ : Type ?u.366422
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
x✝ : (∀ (a : Ordinal), f a < f (succ a)) ∧ ∀ (o : Ordinal), IsLimit o → (bsup o fun x x_1 => f x) = f o
h₁ : ∀ (a : Ordinal), f a < f (succ a)
h₂ : ∀ (o : Ordinal), IsLimit o → (bsup o fun x x_1 => f x) = f o
o : Ordinal
ho : IsLimit o
a : Ordinal
⊢ f o ≤ a ↔ ∀ (b : Ordinal), b < o → f b ≤ a
rw [← h₂ o ho]
no goals
α : Type ?u.366416
β : Type ?u.366419
γ : Type ?u.366422
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : Ordinal → Ordinal
x✝ : (∀ (a : Ordinal), f a < f (succ a)) ∧ ∀ (o : Ordinal), IsLimit o → (bsup o fun x x_1 => f x) = f o
h₁ : ∀ (a : Ordinal), f a < f (succ a)
h₂ : ∀ (o : Ordinal), IsLimit o → (bsup o fun x x_1 => f x) = f o
o : Ordinal
ho : IsLimit o
a : Ordinal
⊢ (bsup o fun x x_1 => f x) ≤ a ↔ ∀ (b : Ordinal), b < o → f b ≤ a
exact bsup_le_iff