insert_ne_self

Mathlib.Data.Set.Insert

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

English

Let s be a subset of α and a an element of α. The set obtained by inserting a into s is different from s if and only if a ∉ s.

Русский

Пусть s ⊆ α и a ∈ α. Множество, полученное добавлением элемента a к s, не равно s тогда и только тогда, когда a ∉ s.

LaTeX

$$$(s \cup \{a\}) \neq s \iff a \notin s$$$

Lean4

theorem insert_ne_self : insert a s ≠ s ↔ a ∉ s := by grind

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

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

Разделы

Аффилиация

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