insert_inj

Mathlib.Data.Set.Insert

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

← MathLib Explorer

English

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

Русский

Если a ∉ s, то insert a s = insert b s подразумевает a = b.

LaTeX

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

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 a s) ha, congr_arg (fun x => insert x s)⟩

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

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

Разделы

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

Аффилиация

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