mem_cons_of_mem

Mathlib.Data.Finset.Insert

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

English

If a ∈ s and b ∉ s, then a ∈ s.cons b s hb.

Русский

Если a ∈ s и b ∉ s, то a ∈ s.cons b s hb.

LaTeX

$$$(ha : a \in s) \Rightarrow a \in cons b s hb$$$

Lean4

theorem mem_cons_of_mem {a b : α} {s : Finset α} {hb : b ∉ s} (ha : a ∈ s) : a ∈ cons b s hb :=
  Multiset.mem_cons_of_mem ha

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

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

Разделы

Аффилиация

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