algebraMap_lt_algebraMap — Mathlib

English

The algebra map preserves strict order: a1 < a2 iff algebraMap a1 < algebraMap a2.

Русский

Отображение алгебра сохраняет строгий порядок: a1 < a2 эквивалентно algebraMap a1 < algebraMap a2.

LaTeX

$$$a_1 < a_2 \iff \text{algebraMap } a_1 < \text{algebraMap } a_2$$$

Lean4

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

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