nmul_nadd_lt — 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' < a \\rightarrow b' < b \\rightarrow a' \\nabla b \\sharp a \\nabla b' < a \\nabla b \\sharp a' \\nabla b'$$$

Lean4

theorem nmul_nadd_lt {a' b' : Ordinal} (ha : a' < a) (hb : b' < b) : a' ⨳ b ♯ a ⨳ b' < a ⨳ b ♯ a' ⨳ b' :=
  by
  conv_rhs => rw [nmul]
  exact csInf_mem (nmul_nonempty a b) a' ha b' hb

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