English
Imaging over intersection distributes: (s1 ∩ s2).map f = s1.map f ∩ s2.map f.
Русский
Образование пересечения через отображение распределяется: (s1 ∩ s2).map f = s1.map f ∩ s2.map f.
LaTeX
$$$ (s_1 \cap s_2).map f = s_1.map f \cap s_2.map f$$$
Lean4
theorem map_inter [DecidableEq α] [DecidableEq β] {f : α ↪ β} (s₁ s₂ : Finset α) :
(s₁ ∩ s₂).map f = s₁.map f ∩ s₂.map f :=
mod_cast Set.image_inter f.injective (s := s₁) (t := s₂)