eq_of_mem_insert_of_notMem

Mathlib.Data.Finset.Insert

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

English

If b ∈ insert a s and b ∉ s, then b = a.

Русский

Если b принадлежит insert a s и b ∉ s, то b = a.

LaTeX

$$$ (b \in insert a s) \to (b \notin s) \Rightarrow b = a$$$

Lean4

theorem eq_of_mem_insert_of_notMem (ha : b ∈ insert a s) (hb : b ∉ s) : b = a :=
  (mem_insert.1 ha).resolve_right hb

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

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

Разделы

Аффилиация

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