insert_idem

Mathlib.Data.Set.Insert

URI: https://scilib.ai/kg/mathlib#Set.insert_idem

English

Inserting the same element twice yields the same set as inserting it once.

Русский

Повторная вставка одного и того же элемента не изменяет множество: 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 : Set α) : insert a (insert a s) = insert a s := by grind

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru