nmul_nadd_le — Mathlib

English

If a' ≤ a and b' ≤ b, then a' ⨳ b ♯ a ⨳ b' ≤ a ⨳ b ♯ a' ⨳ b'.

Русский

Если a' ≤ a и b' ≤ b, то a' ⨳ b ♯ a ⨳ b' ≤ a ⨳ b ♯ a' ⨳ b'.

LaTeX

$$$\\forall a,b,a',b' \\in \\mathrm{Ordinal},\\ a' \\le a \\rightarrow b' \\le b \\rightarrow a' \\nabla b \\sharp a \\nabla b' \\le a \\nabla b \\sharp a' \\nabla b'$$$

Lean4

theorem nmul_nadd_le {a' b' : Ordinal} (ha : a' ≤ a) (hb : b' ≤ b) : a' ⨳ b ♯ a ⨳ b' ≤ a ⨳ b ♯ a' ⨳ b' :=
  by
  rcases lt_or_eq_of_le ha with (ha | rfl)
  · rcases lt_or_eq_of_le hb with (hb | rfl)
    · exact (nmul_nadd_lt ha hb).le
    · rw [nadd_comm]
  · exact le_rfl

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