left_inv

Mathlib.Topology.OpenPartialHomeomorph

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

English

For all x ∈ e.source, e.symm(e(x)) = x.

Русский

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

LaTeX

$$$ \forall x \in e.source:\ e.symm(e(x)) = x.$$$

Lean4

@[simp, mfld_simps]
theorem left_inv {x : X} (h : x ∈ e.source) : e.symm (e x) = x :=
  e.left_inv' h

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

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

Разделы

Аффилиация

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