mk_le_mk — Mathlib

English

For any m,m' ∈ M and s,s' ∈ ℕ+, mk m s ≤ mk m' s' if and only if s'.val · m ≤ s.val · m' in M.

Русский

Для любых $m,m'\\in M$ и $s,s'\\in\\mathbb{N}_{>0}$ выполняется $\\mathrm{mk}(m,s) \\le \\mathrm{mk}(m',s')$ тогда и только если $s'.\\mathrm{val}\\, m \\le s.\\mathrm{val}\\, m'$ в $M$.

LaTeX

$$$\\mathrm{mk}(m,s) \\le \\mathrm{mk}(m',s') \\iff s'.\\text{val} \\cdot m \\le s.\\text{val} \\cdot m' .$$$

Lean4

@[simp]
theorem mk_le_mk {m m' : M} {s s' : ℕ+} : mk m s ≤ mk m' s' ↔ s'.val • m ≤ s.val • m' := by rfl

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