symm — Mathlib

English

If e is an open partial homeomorphism between X and Y and s ⊆ X, t ⊆ Y satisfy that e maps e's source∩s onto e's target∩t, then the inverse map e⁻¹ maps e's target∩t onto e's source∩s.

Русский

Пусть e — открытое частичное гомеоморфизм между X и Y, и s ⊆ X, t ⊆ Y удовлетворяют, что e отображает e.источник ∩ s на e.цель ∩ t; тогда обратное отображение e⁻¹ отображает e.цель ∩ t обратно в e.источник ∩ s.

LaTeX

$$$IsImage(e, s, t) \\Rightarrow IsImage(e^{-1}, t, s)$$$

Lean4

protected theorem symm (h : e.IsImage s t) : e.symm.IsImage t s :=
  h.toPartialEquiv.symm

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