mem_image_equiv

Mathlib.Logic.Equiv.Set

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

← MathLib Explorer

English

For any S ⊆ α and bijection e: α ≃ β, x ∈ e''S iff e⁻¹(x) ∈ S.

Русский

Для любого S ⊆ α и биекции e: α ≃ β верно: x ∈ e''S эквивалентно e⁻¹(x) ∈ S.

LaTeX

$$$x \in e''S \;\Longleftrightarrow\; e^{-1}(x) \in S.$$$

Lean4

@[simp 1001]
theorem _root_.Set.mem_image_equiv {α β} {S : Set α} {f : α ≃ β} {x : β} : x ∈ f '' S ↔ f.symm x ∈ S :=
  Set.ext_iff.mp (f.image_eq_preimage S) x

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

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

Разделы

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

Аффилиация

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