toOpenPartialHomeomorph_right_inv

English

If x lies in the range of f, then f applied to the inverse image of x under the induced open partial homeomorphism returns x: if x ∈ range(f) then f((h.toOpenPartialHomeomorph f).symm x) = x.

Русский

Пусть x принадлежит образу f; тогда f применённое к обратному образу x по открытому частичному гомеоморфизму возвращает x: если x ∈ range(f), то f((h.toOpenPartialHomeomorph f).symm x) = x.

LaTeX

$$$ x \in \mathrm{range}(f) \Rightarrow f((h.toOpenPartialHomeomorph f).symm x) = x $$$

Lean4

theorem toOpenPartialHomeomorph_right_inv {x : Y} (hx : x ∈ Set.range f) :
    f ((h.toOpenPartialHomeomorph f).symm x) = x :=
  by
  rw [← congr_fun (h.toOpenPartialHomeomorph_apply f), OpenPartialHomeomorph.right_inv]
  rwa [toOpenPartialHomeomorph_target]

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