Shelah's ded bound on the traces of a family of finite VC dimension. On an infinite ground set a family of finite VC dimension traces at most ded #A sets, and by mk_image_inter_range_cut_eq_ded the bound is attained. The infiniteness of A is not decorative: see exists_finite_ground_hasVCDimLE_not_mk_image_inter_le_ded.
DeclHasVCDimLE.mk_image_inter_le_ded
∀ {α : Type u} {𝒜 : Set (Set α)} {A : Set α} {d : ℕ},
HasVCDimLE d 𝒜 → A.Infinite → Cardinal.mk ↑((fun x => A ∩ x) '' 𝒜) ≤ ded (Cardinal.mk ↑A)TopicCardinal bounds
Relations
- Limited byMTH.C-2026-6008
No cardinal function smaller than ded bounds the traces, which places ded at the exact strength of the bound.
Asserted byDhruv Gupta
Arguments
| DOI | Author | Date |
|---|---|---|
| MTH.R-2026-6007 | Dhruv Gupta | 2026-09-24T00:00:00Z |
DOIMTH.C-2026-6007
Cite
Verification
- Library
- FLT_Proofs.VCDimGeneralized.VCDimDed
- Statement digest
- ca7e04b50bc8
- First verified
- 2026-09-24T00:00:00Z