ne_insert_of_notMem

Mathlib.Data.Set.Insert

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

English

If a ∉ s, then s ≠ insert a t for any t.

Русский

Если a ∉ s, то s ≠ insert a t для любого t.

LaTeX

$$$a \notin s \Rightarrow s \neq \mathrm{insert}(a,t).$$$

Lean4

theorem ne_insert_of_notMem {s : Set α} (t : Set α) {a : α} : a ∉ s → s ≠ insert a t := by grind

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

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

Разделы

Аффилиация

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