symm_comp_self

Mathlib.MeasureTheory.MeasurableSpace.Embedding

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

English

The composition of a measurable equivalence with its inverse equals the identity on the domain.

Русский

Составление измеримого эквивалента с его обратным является идентичностью на области определения.

LaTeX

$$$$ e^{-1} \circ e = \mathrm{id}. $$$$

Lean4

@[simp]
theorem symm_comp_self (e : α ≃ᵐ β) : e.symm ∘ e = id :=
  funext e.left_inv

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

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

Разделы

Аффилиация

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