image_equiv_eq_preimage_symm

Mathlib.Logic.Equiv.Set

URI: https://scilib.ai/kg/mathlib#Set.image_equiv_eq_preimage_symm

← MathLib Explorer

English

Alias: Set.image_eq_preimage e S = Set.preimage e.symm S for any e and S.

Русский

Псевдоним: Set.image_eq_preimage e S = Set.preimage e.symm S для любых e и S.

LaTeX

$$$\text{Set.image} (e) S = \text{Set.preimage} (e^{-1}) S.$$$

Lean4

/-- Alias for `Equiv.image_eq_preimage` -/
theorem _root_.Set.image_equiv_eq_preimage_symm {α β} (S : Set α) (f : α ≃ β) : f '' S = f.symm ⁻¹' S :=
  f.image_eq_preimage S

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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