map_ne

Mathlib.Analysis.Normed.Affine.Isometry

URI: https://scilib.ai/kg/mathlib#AffineIsometryEquiv.map_ne

English

AffineIsometryEquiv forms a group under composition with identity and inverse given by refl and symm.

Русский

Множество аффинных изометрий образует группу под операцией композиции.

LaTeX

$$$\text{Group}(P \simeq^a_i P)$ with $e_1 \cdot e_2 = e_2 \circ e_1$, identity $\mathrm{refl}$, inverse $e^{-1} = \mathrm{symm}$.$$

Lean4

theorem map_ne {x y : P} (h : x ≠ y) : e x ≠ e y :=
  e.injective.ne h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru