insert_comm — Mathlib

English

Inserting two elements into a finite set is independent of the order: insert(a, insert(b, s)) = insert(b, insert(a, s)).

Русский

Вставка двух элементов в конечное множество не сказывается на порядке: insert(a, insert(b, s)) = insert(b, insert(a, s)).

LaTeX

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

Lean4

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

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