preimage_symm_preimage

Mathlib.Topology.Algebra.Algebra.Equiv

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

English

The preimage under e of the preimage under e.symm of S equals S: e^{-1}( e.symm^{-1}(S) ) = S.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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