mem_of_mem_insert_of_ne

Mathlib.Data.Finset.Insert

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

English

If x is in insert a s and x ≠ a, then x ∈ s.

Русский

Если x ∈ insert a s и x ≠ a, то x ∈ s.

LaTeX

$$$ (x \in insert a s) \wedge x \neq a \Rightarrow x \in s$$$

Lean4

theorem mem_of_mem_insert_of_ne (h : b ∈ insert a s) : b ≠ a → b ∈ s :=
  (mem_insert.1 h).resolve_left

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

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

Разделы

Аффилиация

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