preimage_eq_iff_eq_image

Mathlib.Logic.Equiv.Set

URI: https://scilib.ai/kg/mathlib#Equiv.preimage_eq_iff_eq_image

English

For a bijection e and sets s,t, e^{-1}(s) = t iff s = e[t].

Русский

Для биекции e и подмножеств s,t верно: e^{-1}(s) = t эквивалентно s = e[t].

LaTeX

$$$ e^{-1}(s) = t \iff s = e[t] $$$

Lean4

theorem preimage_eq_iff_eq_image {α β} (e : α ≃ β) (s t) : e ⁻¹' s = t ↔ s = e '' t :=
  Set.preimage_eq_iff_eq_image e.bijective

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

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

Разделы

Аффилиация

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