map_inter — Mathlib

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₂)

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