image_preimage_inter

Mathlib.Data.Set.Image

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

← MathLib Explorer

English

Let f: α → β, S ⊆ α, T ⊆ β. Then f[S ∩ f^{-1}(T)] = T ∩ f[S].

Русский

Пусть f: α → β, S ⊆ α, T ⊆ β. Тогда f[S ∩ f^{-1}(T)] = T ∩ f[S].

LaTeX

$$$f[S \\cap f^{-1}(T)] = T \\cap f[S]$$$

Lean4

theorem image_preimage_inter (f : α → β) (s : Set α) (t : Set β) : f '' (f ⁻¹' t ∩ s) = t ∩ f '' s := by
  simp only [inter_comm, image_inter_preimage]

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

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

Разделы

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

Аффилиация

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