singleton_inter

Mathlib.Data.Finset.Lattice.Lemmas

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

English

For a ∈ s, s ∩ {a} = {a}.

Русский

Для a ∈ s верно s ∩ {a} = {a}.

LaTeX

$$h : a ∈ s → s ∩ {a} = {a}$$

Lean4

@[grind =]
theorem singleton_inter {a : α} {s : Finset α} : { a } ∩ s = if a ∈ s then { a } else ∅ := by
  split_ifs with h <;> simp [h]

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

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

Разделы

Аффилиация

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