algebraMap_mono — Mathlib

English

The algebra map from α to β is monotone with respect to the given orders: if a1 ≤ a2 in α, then algebraMap α β a1 ≤ algebraMap α β a2 in β.

Русский

Функция отображения алгебры из α в β монотонна: если a1 ≤ a2 в α, то algebraMap α β a1 ≤ algebraMap α β a2 в β.

LaTeX

$$$a_1 \le a_2 \quad\Rightarrow\quad \text{algebraMap } \alpha\beta\ a_1 \le \text{algebraMap } \alpha\beta\ a_2$$$

Lean4

@[mono]
theorem algebraMap_mono : Monotone (algebraMap α β) := fun a₁ a₂ ha ↦ by
  simpa only [Algebra.algebraMap_eq_smul_one] using smul_le_smul_of_nonneg_right ha zero_le_one

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