trans_refl

Mathlib.Analysis.Normed.Operator.LinearIsometry

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

English

Composing with the identity (refl) yields the original equivalence: e trans refl = e.

Русский

Сочетание с тождественным переходом даёт исходное эквивалентное отображение: e trans refl = e.

LaTeX

$$$ e.trans(\\mathrm{refl}\\; R_2\\; E_2) = e $$$

Lean4

@[simp]
theorem trans_refl : e.trans (refl R₂ E₂) = e :=
  ext fun _ => rfl

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

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

Разделы

Аффилиация

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