symm_preimage_preimage

Mathlib.Topology.Algebra.Algebra.Equiv

URI: https://scilib.ai/kg/mathlib#ContinuousAlgEquiv.symm_preimage_preimage

English

Preimage of a preimage identity: e.symm^{-1}( e^{-1}(S) ) = S.

Русский

Обратное образ предобраза даёт S: e.symm^{-1}( e^{-1}(S) ) = S.

LaTeX

$$$e^{\mathrm{symm}}^{-1}(e^{-1}(S)) = S$$$

Lean4

@[simp]
theorem symm_preimage_preimage (e : A ≃A[R] B) (S : Set B) : e.symm ⁻¹' (e ⁻¹' S) = S :=
  e.toEquiv.symm_preimage_preimage S

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

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

Разделы

Аффилиация

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