nmul_lt_nmul_of_pos_right — Mathlib

English

If a' < a, b' < b, c' < c, then a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' < a ⨳ b ⨳ c ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'.

Русский

Если a' < a, b' < b, c' < c, то ... неравенство между двумя сложными выражениями (nmul_nadd_lt₃).

LaTeX

$$$\\forall a,b,a',b',c,c' \\in \\mathrm{Ordinal},\\ a' < a \\rightarrow b' < b \\rightarrow c' < c \\rightarrow \\text{nmul_nadd_lt₃}(a,b,c,a',b',c')$$$

Lean4

theorem nmul_lt_nmul_of_pos_right (h₁ : a < b) (h₂ : 0 < c) : a ⨳ c < b ⨳ c :=
  lt_nmul_iff.2 ⟨a, h₁, 0, h₂, by simp⟩

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