insert_inter — Mathlib

English

A refined version of the previous fact: intersection with an insertion equals insertion into the intersection if the element is in the second set, otherwise unchanged.

Русский

Уточнённая версия: пересечение с вставкой равно вставке в пересечение, если элемент содержится во втором множестве, иначе не меняется.

LaTeX

$$$S_1 \cap (S_2 \cup \{a\}) = \begin{cases} (S_1 \cap S_2) \cup \{a\} & a \in S_2 \\ S_1 \cap S_2 & a \notin S_2 \end{cases}$$$

Lean4

@[grind =]
theorem insert_inter {s₁ s₂ : Finset α} {a : α} : s₁ ∩ insert a s₂ = if a ∈ s₁ then insert a (s₁ ∩ s₂) else s₁ ∩ s₂ :=
  by split_ifs <;> simp [*]

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