self_trans_symm

Mathlib.MeasureTheory.MeasurableSpace.Embedding

URI: https://scilib.ai/kg/mathlib#MeasurableEquiv.self_trans_symm

English

Composition of a measurable equivalence with its inverse is the identity on the domain.

Русский

Сочетание измеримого эквивалента с его обратной трансформацией даёт идентичность на области определения.

LaTeX

$$$$ e_{symm} \circ e = \mathrm{id}. $$$$

Lean4

@[simp]
theorem self_trans_symm (e : α ≃ᵐ β) : e.trans e.symm = refl α :=
  ext e.symm_comp_self

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

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

Разделы

Аффилиация

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