insert_inj

Mathlib.Data.Finset.Insert

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

← MathLib Explorer

English

If a ∉ s, then insert a s = insert b s iff a = b.

Русский

Если a ∉ s, то insert a s = insert b s эквивалентно a = b.

LaTeX

$$$a \\notin s \\Rightarrow (\\operatorname{insert}(a,s) = \\operatorname{insert}(b,s) \\iff a = b)$$$

Lean4

theorem insert_inj (ha : a ∉ s) : insert a s = insert b s ↔ a = b :=
  ⟨fun h => eq_of_mem_insert_of_notMem (h ▸ mem_insert_self _ _) ha, congr_arg (insert · s)⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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