English
If a' ≤ a, b' ≤ b, c' ≤ c then the corresponding nmul_nadd_le₃ inequality holds between the three-way nmul-nadd expressions.
Русский
Если a' ≤ a, b' ≤ b, c' ≤ c, то выполняется неравенство nmul_nadd_le₃ между тройственными nmul-nadd выражениями.
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'))\\left(((a.nmul b).nmul c).nadd ((a'.nmul b').nmul c)).nadd ((a.nmul b').nmul c')\\right)$$$
Lean4
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
simpa only [nadd_nmul, ← nadd_assoc] using nmul_nadd_le (nmul_nadd_le ha hb) hc
