vcDim_compress_le — Mathlib

English

Down-compression does not increase VC-dimension: (Down(a,𝒜)).vcDim ≤ 𝒜.vcDim.

Русский

Сжатие по элементу a не увеличивает VC-размерность: (Down(a,𝒜)).vcDim ≤ 𝒜.vcDim.

LaTeX

$$$vcDim( (Down.compression\\ a\\ 𝒜) ) \\le vcDim(𝒜)$$$

Lean4

/-- Down-compressing decreases the VC-dimension. -/
theorem vcDim_compress_le (a : α) (𝒜 : Finset (Finset α)) : (𝓓 a 𝒜).vcDim ≤ 𝒜.vcDim :=
  sup_mono <| shatterer_compress_subset_shatterer _ _

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