English
A deprecated variant of nmul_nadd_le₃ with mirrored structure; shows equivalence by converting to nat ordinal arithmetic.
Русский
Устаревшая версия nmul_nadd_le₃ с зеркальным построением; эквивалентность через перевод в нормальные натуральные ординалы.
LaTeX
$$$\\forall a,b,c,a',b',c' \\in \\mathrm{Ordinal},\\ a' \\le a \\rightarrow b' \\le b \\rightarrow c' \\le c \\rightarrow \\text{le}\\left(((((a'.nmul (b.nmul c)).nadd (a.nmul (b'.nmul c))).nadd (a.nmul (b.nmul c))).nadd (a'.nmul (b'.nmul c'))).nadd ( (a.nmul (b.nmul c)).nadd (a'.nmul (b'.nmul c))).nadd ( (a'.nmul b).nmul c')\\right) \\left(((((a.nmul (b.nmul c)).nadd (a'.nmul (b'.nmul c))).nadd (a'.nmul (b.nmul c))).nadd (a.nmul (b'.nmul c'))).nadd ((a.nmul (b.nmul c)).nadd (a'.nmul (b'.nmul c))).nadd (a'.nmul (b.nmul c')))$$$$
Lean4
@[deprecated nmul_nadd_le₃ (since := "2024-11-19")]
theorem nmul_nadd_le₃' {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
simp only [nmul_comm _ (_ ⨳ _)]
convert nmul_nadd_le₃ hb hc ha using 1 <;> (simp only [nadd_eq_add, NatOrdinal.toOrdinal_toNatOrdinal]; abel_nf)
