erase_insert — Mathlib

English

Let s be a Finite set and a be an element not in s. Then erasing a from the insertion of a into s yields s, i.e., erase(insert(a, s), a) = s.

Русский

Пусть s — конечное множество и a ∉ s. Тогда удаление a из вставки a в s возвращает s: erase(insert(a, s), a) = s.

LaTeX

$$$a \\notin s \\implies \\operatorname{erase}(\\operatorname{insert}(a,s), a) = s$$$

Lean4

theorem erase_insert {a : α} {s : Finset α} (h : a ∉ s) : erase (insert a s) a = s := by grind

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