image_eq_preimage

Mathlib.Topology.Algebra.Algebra.Equiv

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

English

For any set S, the image of S under e equals the preimage of S under e.symm, i.e., e[S] = e.symm^{-1}[S].

Русский

Для множества S выполняется равенство образа S через e и предобраза S через e.symm: e[S] = e.symm^{-1}[S].

LaTeX

$$$e[S] = e^{-1}[S]$$$

Lean4

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

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

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

Разделы

Аффилиация

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