right_inv

Mathlib.Topology.OpenPartialHomeomorph

URI: https://scilib.ai/kg/mathlib#OpenPartialHomeomorph.right_inv

English

For all y ∈ e.target, e(e.symm(y)) = y.

Русский

Для всех y ∈ e.target выполняется e(e.symm(y)) = y.

LaTeX

$$$ \forall y \in e.target:\ e(e.symm(y)) = y.$$$

Lean4

@[simp, mfld_simps]
theorem right_inv {x : Y} (h : x ∈ e.target) : e (e.symm x) = x :=
  e.right_inv' h

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

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

Разделы

Аффилиация

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