insert_inter_of_notMem — Mathlib

English

If a ∉ S2, then inserting a into S1 does not change the intersection with S2: (S1 ∪ {a}) ∩ S2 = S1 ∩ S2.

Русский

Если a не принадлежит S2, пересечение не изменится при добавлении a в S1: (S1 ∪ {a}) ∩ S2 = S1 ∩ S2.

LaTeX

$$$a \notin S_2 \Rightarrow (S_1 \cup \{a\}) \cap S_2 = S_1 \cap S_2$$$

Lean4

@[simp]
theorem insert_inter_of_notMem {s₁ s₂ : Finset α} {a : α} (h : a ∉ s₂) : insert a s₁ ∩ s₂ = s₁ ∩ s₂ :=
  ext fun x => by
    have : ¬(x = a ∧ x ∈ s₂) := by rintro ⟨rfl, H⟩; exact h H
    simp only [mem_inter, mem_insert, or_and_right, this, false_or]

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