eq_of_mem_of_notMem_erase

Mathlib.Data.Finset.Erase

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

← MathLib Explorer

English

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

Русский

Если b ∈ s и b ∉ erase s a, тогда b = a.

LaTeX

$$$ \text{mem}(s,b) \land \lnot \text{mem}(s,a,b) \Rightarrow b = a $$$

Lean4

/-- An element of `s` that is not an element of `erase s a` must be`a`. -/
theorem eq_of_mem_of_notMem_erase (hs : b ∈ s) (hsa : b ∉ s.erase a) : b = a := by grind

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

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

Разделы

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

Аффилиация

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