image_preimage_eq

Mathlib.Data.Set.Image

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

← MathLib Explorer

English

If f is surjective, then f''(f^{-1}(S)) = S for any S.

Русский

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

LaTeX

$$$$ f''(f^{-1}(S)) = S \quad \text{if } f \text{ is surjective}. $$$$

Lean4

@[simp]
theorem image_preimage_eq {f : α → β} (s : Set β) (h : Surjective f) : f '' (f ⁻¹' s) = s :=
  Subset.antisymm (image_preimage_subset f s) fun x hx =>
    let ⟨y, e⟩ := h x
    ⟨y, by grind⟩

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

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

Разделы

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

Аффилиация

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