α : Type ?u.312782
β : Type ?u.312785
γ : Type ?u.312788
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
h : bsup o f = 0
i : Ordinal
hi : i < o
⊢ f i hi = 0
α : Type ?u.312782
β : Type ?u.312785
γ : Type ?u.312788
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
⊢ bsup o f = 0 ↔ ∀ (i : Ordinal) (hi : i < o), f i hi = 0
refine'
  ⟨fun h i hi => _, fun h =>
    le_antisymm (bsup_le fun i hi => Ordinal.le_zero.2 (h i hi)) (Ordinal.zero_le _)⟩
α : Type ?u.312782
β : Type ?u.312785
γ : Type ?u.312788
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
h : bsup o f = 0
i : Ordinal
hi : i < o
⊢ f i hi ≤ bsup o f
α : Type ?u.312782
β : Type ?u.312785
γ : Type ?u.312788
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
h : bsup o f = 0
i : Ordinal
hi : i < o
⊢ f i hi = 0
rw [← Ordinal.le_zero, ← h]
no goals
α : Type ?u.312782
β : Type ?u.312785
γ : Type ?u.312788
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
f : (a : Ordinal) → a < o → Ordinal
h : bsup o f = 0
i : Ordinal
hi : i < o
⊢ f i hi ≤ bsup o f
exact le_bsup f i hi