shatters_of_forall_subset

Mathlib.Combinatorics.SetFamily.Shatter

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

English

If ∀ t ⊆ s, t ∈ 𝒜, then 𝒜.Shatters s.

Русский

Если ∀ t ⊆ s, t ∈ 𝒜, тогда 𝒜.Shatters s.

LaTeX

$$$\big( \forall t \subseteq s, t \in 𝒜 \big) \Rightarrow 𝒜.Shatters(s)$$$

Lean4

theorem shatters_of_forall_subset (h : ∀ t, t ⊆ s → t ∈ 𝒜) : 𝒜.Shatters s := fun t ht ↦ ⟨t, h _ ht, inter_eq_right.2 ht⟩

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

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

Разделы

Аффилиация

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