image_inter_preimage — Mathlib

English

For any function f and sets S ⊆ A, T ⊆ B, the image of the intersection S ∩ f^{-1}(T) under f equals the intersection of the image of S with T: f[S ∩ f^{-1}(T)] = f[S] ∩ T.

Русский

Для любой функции f и множеств S ⊆ A, T ⊆ B выполняется: образ множества S ∩ f^{-1}(T) при отображении f совпадает с пересечением образа S и T: f[S ∩ f^{-1}(T)] = f[S] ∩ T.

LaTeX

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

Lean4

theorem image_inter_preimage (f : α → β) (s : Set α) (t : Set β) : f '' (s ∩ f ⁻¹' t) = f '' s ∩ t := by grind

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