preimage_image_eq

Mathlib.Data.Set.Image

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

← MathLib Explorer

English

If f is injective, then f^{-1}(f[S]) = S for any S.

Русский

Если f инъективна, то f^{-1}(f[S]) = S для любого S.

LaTeX

$$$$ f^{-1}(f[S]) = S \quad \text{if } f \text{ is injective}. $$$$

Lean4

@[simp]
theorem preimage_image_eq {f : α → β} (s : Set α) (h : Injective f) : f ⁻¹' (f '' s) = s :=
  Subset.antisymm (fun _ ⟨_, hy, e⟩ => h e ▸ hy) (subset_preimage_image f s)

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

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

Разделы

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

Аффилиация

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