op : Ordinal → Ordinal → Ordinal
a o : Ordinal
hao : a < o
H : IsNormal (op a)
ho : Principal op o
ho' : IsLimit o
⊢ op a o ≤ o
op : Ordinal → Ordinal → Ordinal
a o : Ordinal
hao : a < o
H : IsNormal (op a)
ho : Principal op o
ho' : IsLimit o
⊢ op a o = o
refine' le_antisymm _ (H.self_le _)
op : Ordinal → Ordinal → Ordinal
a o : Ordinal
hao : a < o
H : IsNormal (op a)
ho : Principal op o
ho' : IsLimit o
⊢ ∀ (i : Ordinal), i < o → op a i ≤ o
op : Ordinal → Ordinal → Ordinal
a o : Ordinal
hao : a < o
H : IsNormal (op a)
ho : Principal op o
ho' : IsLimit o
⊢ op a o ≤ o
rw [← IsNormal.bsup_eq.{u, u} H ho', bsup_le_iff]
no goals
op : Ordinal → Ordinal → Ordinal
a o : Ordinal
hao : a < o
H : IsNormal (op a)
ho : Principal op o
ho' : IsLimit o
⊢ ∀ (i : Ordinal), i < o → op a i ≤ o
exact fun b hbo => (ho hao hbo).le