image_eq_preimage

Mathlib.Algebra.Ring.Equiv

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

English

For a ring isomorphism e, the image of a set s under e equals the preimage of s under e.symm.

Русский

Для кольцевого изоморфизма e образ множества s равен предобразу множества s под e.symm.

LaTeX

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

Lean4

theorem image_eq_preimage (e : R ≃+* S) (s : Set R) : e '' s = e.symm ⁻¹' s :=
  e.toEquiv.image_eq_preimage s

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

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

Разделы

Аффилиация

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