erase_insert_of_ne — Mathlib

English

Let a, b be elements and s a Finset with a ≠ b. Then erase(insert(a, s), b) = insert(a, erase(s, b)).

Русский

Пусть a, b — элементы и s — Finset при условии a ≠ b. Тогда erase(insert(a, s), b) = insert(a, erase(s, b)).

LaTeX

$$a \\neq b \\rightarrow \\operatorname{erase}(\\operatorname{insert}(a,s), b) = \\operatorname{insert}(a, \\operatorname{erase}(s,b))$$

Lean4

theorem erase_insert_of_ne {a b : α} {s : Finset α} (h : a ≠ b) : erase (insert a s) b = insert a (erase s b) := by
  grind

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