insert_comm — Mathlib

English

Insertion is commutative: inserting a into insert b s yields the same set as inserting b into insert a s.

Русский

Вставка элемента в множество коммутативна: вставка a в вставку b s эквивалентна вставке b в вставку a s.

LaTeX

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

Lean4

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

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