inter_singleton_of_notMem

Mathlib.Data.Finset.Lattice.Lemmas

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

English

If a ∉ s, then s ∩ {a} = ∅.

Русский

Если a ∉ s, то s ∩ {a} = ∅.

LaTeX

$$h : a ∉ s → s ∩ {a} = ∅$$

Lean4

@[simp]
theorem inter_singleton_of_notMem {a : α} {s : Finset α} (h : a ∉ s) : s ∩ { a } = ∅ := by
  rw [inter_comm, singleton_inter_of_notMem h]

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

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

Разделы

Аффилиация

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