inter_insert — Mathlib

English

The intersection with an insertion is piecewise: S1 ∩ (insert a S2) = { a }-case depending on whether a ∈ S2.

Русский

Пересечение с вставкой элемента имеет разрез по условию: S1 ∩ (S2 ∪ {a}) равно либо {a} ∪ (S1 ∩ S2), если a ∈ S2, либо S1 ∩ S2, если a ∉ S2.

LaTeX

$$$S_1 \cap (S_2 \cup \{a\}) = \begin{cases} (S_1 \cap S_2) \cup \{a\} & \text{если } a \in S_2 \\ S_1 \cap S_2 & \text{если } a \notin S_2 \end{cases}$$$

Lean4

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

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