insert_inter_of_mem — Mathlib

English

If a ∈ S2, then inserting a into S1 commutes with intersection: (S1 ∪ {a}) ∩ S2 = {a} ∪ (S1 ∩ S2).

Русский

Если a принадлежит S2, то добавление a в S1 и взятие пересечения с S2 равно объединению {a} с пересечением S1 и S2.

LaTeX

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

Lean4

@[simp]
theorem insert_inter_of_mem {s₁ s₂ : Finset α} {a : α} (h : a ∈ s₂) : insert a s₁ ∩ s₂ = insert a (s₁ ∩ s₂) :=
  ext fun x => by
    have : x = a ∨ x ∈ s₂ ↔ x ∈ s₂ := or_iff_right_of_imp <| by rintro rfl; exact h
    simp only [mem_inter, mem_insert, or_and_left, this]

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