algebraMap_le_algebraMap — Mathlib

English

A variant for gcongr: if a1 ≤ a2 in α, then algebraMap α β a1 ≤ algebraMap α β a2 in β, i.e. the algebra map is order-preserving in the gcongr setting.

Русский

Вариант для gcongr: если a1 ≤ a2 в α, то algebraMap α β a1 ≤ algebraMap α β a2 в β, то есть отображение алгебры сохраняет порядок в настройке gcongr.

LaTeX

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

Lean4

/-- A version of `algebraMap_mono` for use by `gcongr` since it currently does not preprocess
`Monotone` conclusions. -/
@[gcongr]
protected theorem algebraMap_le_algebraMap {a₁ a₂ : α} (ha : a₁ ≤ a₂) : algebraMap α β a₁ ≤ algebraMap α β a₂ :=
  algebraMap_mono _ ha

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