symm_image_image — Mathlib

English

Further symmetry: the double image under inverse and forward equals the original set.

Русский

Дополнительная симметрия: двойной образ под обратным и прямым отображением возвращает исходное множество.

LaTeX

$$$\operatorname{Set.image}(e^{\mathrm{symm}})(\operatorname{Set.image}(e)(s)) = s$$$

Lean4

theorem symm_image_image (e : P₁ ≃ᴬ[k] P₂) (s : Set P₁) : e.symm '' (e '' s) = s :=
  e.toEquiv.symm_image_image s

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