card_le_vcDim

Mathlib.Combinatorics.SetFamily.Shatter

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

English

If s is shattered by 𝒜, then |s| ≤ 𝒜.vcDim.

Русский

Если s раскатано 𝒜, то |s| ≤ 𝒜.vcDim.

LaTeX

$$$\\text{if } 𝒜.Shatters s \\text{ then } |s| \\le \\mathcal{A}.vcDim$$$

Lean4

theorem card_le_vcDim (hs : 𝒜.Shatters s) : #s ≤ 𝒜.vcDim :=
  le_sup <| mem_shatterer.2 hs

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

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

Разделы

Аффилиация

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