insert_eq_self

Mathlib.Data.Finset.Insert

URI: https://scilib.ai/kg/mathlib#Finset.insert_eq_self

English

The insert operation changes the Finset if and only if the inserted element is not already present.

Русский

Вставка изменяет Finset тогда, когда вставляемый элемент ранее не присутствовал.

LaTeX

$$$insert\ a\ s \neq s \iff a \notin s$$$

Lean4

@[simp]
theorem insert_eq_self : insert a s = s ↔ a ∈ s := by grind

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

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

Разделы

Аффилиация

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