mul_refl

Mathlib.Analysis.Normed.Operator.LinearIsometry

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

English

The unit element 1 in the isometry equivalence space is the reflexive map.

Русский

Единичный элемент 1 в пространстве эквивалентностей изометрии равен рефлексивному отображению.

LaTeX

$$$ 1 = \mathrm{refl}_{R} E $$$

Lean4

@[simp]
theorem mul_refl (e : E ≃ₗᵢ[R] E) : e * refl _ _ = e :=
  refl_trans _

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

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

Разделы

Аффилиация

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