The full trace family cannot replace the determined traces in mk_determined_le_mk_shatters: the half-line cuts over ℚ trace continuum-many sets while shattering only countably many.
Declnot_mk_image_inter_le_mk_shatters
¬Cardinal.mk ↑((fun x => Set.univ ∩ x) '' Set.range fun r => {q | ↑q < r}) ≤
Cardinal.mk ↑{B | B ⊆ Set.univ ∧ Shatters (Set.range fun r => {q | ↑q < r}) B}Relations
- LimitsMTH.C-2026-6003
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-6004 | Dhruv Gupta | 2026-09-24T00:00:00Z |
DOIMTH.C-2026-6004
Cite
Verification
- Library
- FLT_Proofs.VCDimGeneralized.VCDimCardinal
- Statement digest
- f4acdbbf80ec
- First verified
- 2026-09-24T00:00:00Z