nadd_assoc — Mathlib

English

Natural addition is associative: (a ♯ b) ♯ c = a ♯ (b ♯ c).

Русский

У натурального сложения операция ассоциативна: (a ♯ b) ♯ c = a ♯ (b ♯ c).

LaTeX

$$$(a \# b) \# c = a \# (b \# c)$$$

Lean4

theorem nadd_assoc (a b c) : a ♯ b ♯ c = a ♯ (b ♯ c) :=
  by
  unfold nadd
  rw [iSup_nadd_of_monotone fun a' ↦ succ (a' ♯ c), iSup_nadd_of_monotone fun b' ↦ succ (a ♯ b'), max_assoc]
  · congr <;> ext x <;> cases x <;> apply congr_arg _ (nadd_assoc _ _ _)
  · exact succ_mono.comp fun x y h ↦ nadd_le_nadd_left h _
  · exact succ_mono.comp fun x y h ↦ nadd_le_nadd_right h _
termination_by (a, b, c)

Похожие утверждения