eq_preimage_iff_image_eq

Mathlib.Logic.Equiv.Set

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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