exists_inter_eq_singleton

Mathlib.Combinatorics.SetFamily.Shatter

URI: https://scilib.ai/kg/mathlib#Finset.Shatters.exists_inter_eq_singleton

English

If 𝒜 shatters s and a ∈ s, then there exists t ∈ 𝒜 with s ∩ t = {a}.

Русский

Если 𝒜 шатрирует s и a ∈ s, то существует t ∈ 𝒜 такое, что s ∩ t = {a}.

LaTeX

$$$\exists t \in 𝒜,\ s \cap t = \{ a \}$$$

Lean4

theorem exists_inter_eq_singleton (hs : Shatters 𝒜 s) (ha : a ∈ s) : ∃ t ∈ 𝒜, s ∩ t = { a } :=
  hs <| singleton_subset_iff.2 ha

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

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

Разделы

Аффилиация

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