insert_idem — Mathlib

English

Inserting the same element twice is the same as inserting it once: insert(a, insert(a, s)) = insert(a, s).

Русский

Повторная вставка одного и того же элемента эквивалентна одной вставке: insert(a, insert(a, s)) = insert(a, s).

LaTeX

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

Lean4

theorem insert_idem (a : α) (s : Finset α) : insert a (insert a s) = insert a s := by grind

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