The cardinal Pajor inequality for determined traces: the traces of 𝒜 on A that are determined by finitely many points inject into the shattered subsets, with no hypotheses. Unlike the ℕ∞-valued encard_determined_le_encard_shatters, this bounds genuine cardinalities; the full trace family cannot replace the determined traces (not_mk_image_inter_le_mk_shatters).
Declmk_determined_le_mk_shatters
∀ {α : Type u_1} {𝒜 : Set (Set α)} {A : Set α},
Cardinal.mk ↑{t | t ∈ (fun x => A ∩ x) '' 𝒜 ∧ ∃ F, F.Finite ∧ ∀ t' ∈ (fun x => A ∩ x) '' 𝒜, t' ∩ F = t ∩ F → t' = t} ≤
Cardinal.mk ↑{B | B ⊆ A ∧ Shatters 𝒜 B}Relations
- Limited byMTH.C-2026-6004
The full trace family cannot replace the determined traces: the half-line cuts over the rationals trace continuum-many sets while shattering only countably many.
Asserted byDhruv Gupta
Arguments
| DOI | Author | Date |
|---|---|---|
| MTH.R-2026-6003 | Dhruv Gupta | 2026-09-24T00:00:00Z |
DOIMTH.C-2026-6003
Cite
Verification
- Library
- FLT_Proofs.VCDimGeneralized.VCDimCardinal
- Statement digest
- a4cc459dcd62
- First verified
- 2026-09-24T00:00:00Z