map_ne

Mathlib.Analysis.Normed.Operator.LinearIsometry

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

English

If x ≠ y then e x ≠ e y.

Русский

Если x ≠ y, то e x ≠ e y.

LaTeX

$$$ x \neq y \Rightarrow e(x) \neq e(y) $$$

Lean4

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

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

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

Разделы

Аффилиация

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