mem_of_mem_cons_of_ne

Mathlib.Data.Finset.Insert

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

← MathLib Explorer

English

If i ∈ cons a s ha and i ≠ a, then i ∈ s.

Русский

Если i ∈ cons a s ha и i ≠ a, тогда i ∈ s.

LaTeX

$$$(hi : i \in cons\ a\ s ha) (hia : i \neq a) : i \in s$$$

Lean4

theorem mem_of_mem_cons_of_ne {s : Finset α} {a : α} {has} {i : α} (hi : i ∈ cons a s has) (hia : i ≠ a) : i ∈ s :=
  (mem_cons.1 hi).resolve_left hia

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

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

Разделы

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

Аффилиация

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