exists_superset

Mathlib.Combinatorics.SetFamily.Shatter

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

English

If 𝒜.Shatters s, then there exists t ∈ 𝒜 with s ⊆ t.

Русский

Если 𝒜.Shatters s, то существует t ∈ 𝒜 с s ⊆ t.

LaTeX

$$$\mathcal{A}.Shatters(s) \Rightarrow \exists t \in 𝒜\; (s \subseteq t)$$$

Lean4

theorem exists_superset (h : 𝒜.Shatters s) : ∃ t ∈ 𝒜, s ⊆ t :=
  let ⟨t, ht, hst⟩ := h Subset.rfl;
  ⟨t, ht, inter_eq_left.1 hst⟩

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

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

Разделы

Аффилиация

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