English
Triple-nested inequality: if a' < a, b' < b, c' < c then a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' < a ⨳ b ⨳ c ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'.
Русский
Условие строгого неравенства в троичной вложенности nmul_nadd_lt₃
LaTeX
$$$\\forall a,b,c,a',b',c' \\in \\mathrm{Ordinal},\\ a' < a \\rightarrow b' < b \\rightarrow c' < c \\rightarrow \\text{lt}(((a'.nmul b).nmul c).nadd ((a.nmul b').nmul c)).nadd ((a'.nmul b').nmul c'))(((a.nmul b).nmul c).nadd ((a'.nmul b').nmul c)).nadd ((a'.nmul b).nmul c'))$$$
Lean4
theorem nmul_nadd_lt₃ {a' b' c' : Ordinal} (ha : a' < a) (hb : b' < b) (hc : c' < c) :
a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' < a ⨳ b ⨳ c ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c' := by
simpa only [nadd_nmul, ← nadd_assoc] using nmul_nadd_lt (nmul_nadd_lt ha hb) hc
