map_target — Mathlib

English

If x is in the target, then the inverse image under the open partial homeomorphism lies in the source.

Русский

Если x принадлежит цели, то обратное изображение под гомеоморфизмом имеет место быть в источнике.

LaTeX

$$$\forall x\in e.target,\ e.toOpenPartialHomeomorph.symm x \in e.source$$$

Lean4

theorem map_target {x : B × F} (hx : x ∈ e.target) : e.toOpenPartialHomeomorph.symm x ∈ e.source :=
  e.toOpenPartialHomeomorph.map_target hx

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