map_sdiff — Mathlib

English

Mapping preserves set difference: (s1 \ s2).map f = s1.map f \ s2.map f.

Русский

Образ через разность множеств сохраняется: (s1 \ s2).map f = s1.map f \ s2.map f.

LaTeX

$$$ (s_1 \\ s_2).map f = s_1.map f \\ s_2.map f$$$

Lean4

theorem map_sdiff [DecidableEq α] [DecidableEq β] {f : α ↪ β} (s₁ s₂ : Finset α) :
    (s₁ \ s₂).map f = s₁.map f \ s₂.map f :=
  mod_cast Set.image_diff f.injective (s := s₁) (t := s₂)

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