limit Ordinal smaller than sum of smaller ordinals

Stream: Is there code for X?

[Jakub Nowak]

theorem Ordinal.add_lt_of_lt_of_lt_of_isSuccPrelimit {o₁ o₂ o : Ordinal}
    (h : Order.IsSuccPrelimit o) (h₁ : o₁ < o) (h₂ : o₂ < o) : o₁ + o₂ < o

I think this is true for Ordinals? Maybe it's present in mathlib with some more generic assumptions?

[Jakub Nowak]

nvm, that's obviously not true for ω + ω.

[Jakub Nowak]

Ah, this property is defined as Ordinal.Principal (fun x1 x2 => x1 + x2). docs#Ordinal.principal_add_iff_zero_or_omega0_opow characterizes all ordinals that have that property.