map_target

Mathlib.Topology.OpenPartialHomeomorph

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

English

If y ∈ e.target, then e.symm(y) ∈ e.source.

Русский

Если y ∈ e.target, то e.symm(y) ∈ e.source.

LaTeX

$$$ \forall y \in e.target,\ e.symm(y) \in e.source.$$$

Lean4

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

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

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

Разделы

Аффилиация

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