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
ThesisStepDefinition
- Declnot_mk_image_inter_le_mk_shattersDeclaration kindtheorem
¬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} - Declcut_injectiveDeclaration kindtheorem
Function.Injective cut✝
- Declcountable_setOf_shatters_range_cutDeclaration kindtheorem
{B | B ⊆ Set.univ ∧ Shatters (Set.range cut✝) B}.Countable - Declsubsingleton_of_shatters_range_cutDeclaration kindtheorem
∀ {B : Set ℚ}, Shatters (Set.range cut✝) B → B.Subsingleton A set family
𝒜shatters a setAif all subsets ofAcan be obtained as the intersection ofAwith some element of the set family. We also say thatAis traced by𝒜.{α : Type u_1} → [SemilatticeInf α] → Set α → α → Prop- Definitioncutdef
ℝ → Set ℚ
DOIMTH.R-2026-6004
Cite
Verification
- Replay
- accepted
- Axioms
- Classical.choiceQuot.soundpropext
- Statement identity
- not-applicable
- Substrate
- Lean 4 kernel v4.31.0
- Dictionary pin
- design-lab@5802df4 · initial
- Frozen export
- ace4eebd4529
- Verified
- 2026-09-24T00:00:00Z