ofUnits_strictMono — Mathlib

English

The map ofUnits is strictly monotone with respect to the lattice order: if S < T then S.ofUnits < T.ofUnits.

Русский

Отображение ofUnits строго монотонно по отношению к порядку по частичным упорядочениям.

LaTeX

$$$S < T \\Rightarrow S^{\\mathrm{ofUnits}} < T^{\\mathrm{ofUnits}}$$$

Lean4

@[to_additive]
theorem ofUnits_strictMono : StrictMono (ofUnits (M := M)) :=
  ofUnits_units_gci.strictMono_l

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