No cardinal function strictly smaller than ded bounds the traces of a family of finite VC dimension. For every infinite κ and every lam < ded κ there is a family of VC dimension 1 on a ground set of size exactly κ tracing more than lam sets. Together with HasVCDimLE.mk_image_inter_le_ded, which caps those traces at ded #A, this places ded at the exact strength of the bound.
The conclusion cannot be strengthened to a family tracing exactly ded κ sets. Chernikov and Shelah, On the number of Dedekind cuts and two-cardinal models of dependent theories, note after their definition of ded κ that "in general the supremum need not be attained", so at such a κ no family attains it and quantifying below the supremum is the available form. At κ = ℵ₀ the supremum is attained, by mk_image_inter_range_cut_eq_ded.
∀ {κ : Cardinal.{u}},
Cardinal.aleph0 ≤ κ →
∀ {lam : Cardinal.{u}},
lam < ded κ → ∃ α 𝒜 A, Cardinal.mk ↑A = κ ∧ HasVCDimLE 1 𝒜 ∧ lam < Cardinal.mk ↑((fun x => A ∩ x) '' 𝒜)Relations
- LimitsMTH.C-2026-6007
No cardinal function smaller than ded bounds the traces, which places ded at the exact strength of the bound.
Asserted byDhruv Gupta
- Declno_smaller_boundDeclaration kindtheorem
∀ {κ : Cardinal.{u}}, Cardinal.aleph0 ≤ κ → ∀ {lam : Cardinal.{u}}, lam < ded κ → ∃ α 𝒜 A, Cardinal.mk ↑A = κ ∧ HasVCDimLE 1 𝒜 ∧ lam < Cardinal.mk ↑((fun x => A ∩ x) '' 𝒜) - Declone_mem_dedSet'Declaration kindtheorem
∀ (κ : Cardinal.{u}), 1 ∈ dedSet'✝ κUsed by
- DeclisStrictlyDenseIn_empty_punitDeclaration kindtheorem
IsStrictlyDenseIn ∅
Used by
- Declexists_family_of_isStrictlyDenseInDeclaration kindtheorem
The witness attached to a strictly dense subset: a family of VC dimension
1on a ground set of size exactlyκwhose traces are at least as many as the points ofJ.∀ {κ : Cardinal.{u}} {J : Type u} [inst : LinearOrder J] {E : Set J}, Cardinal.aleph0 ≤ κ → Cardinal.mk ↑E ≤ κ → IsStrictlyDenseIn E → ∃ α 𝒜 A, Cardinal.mk ↑A = κ ∧ HasVCDimLE 1 𝒜 ∧ Cardinal.mk J ≤ Cardinal.mk ↑((fun x => A ∩ x) '' 𝒜)Used by
- Declmk_padGroundDeclaration kindtheorem
∀ {κ : Cardinal.{u}} {J P : Type u} {E : Set J}, Cardinal.aleph0 ≤ κ → Cardinal.mk ↑E ≤ κ → Cardinal.mk P = κ → Cardinal.mk ↑(padGround✝ E) = κ - DeclisChain_padCutsDeclaration kindtheorem
∀ (J P : Type u) [inst : LinearOrder J], IsChain (fun x1 x2 => x1 ⊆ x2) (padCuts✝ J P)
- Declinter_padCuts_neDeclaration kindtheorem
A point of
Estrictly betweenjandj'separates the two traces: it lies in the trace atj'and, being abovej, not in the trace atj.∀ {J P : Type u} [inst : LinearOrder J] {E : Set J} {j j' e : J}, e ∈ E → j < e → e < j' → padGround✝ E ∩ Sum.inl '' {a | a < j} ≠ padGround✝ E ∩ Sum.inl '' {a | a < j'} - DeclhasVCDimLE_one_of_isChainDeclaration kindtheorem
A family linearly ordered by inclusion has VC dimension at most
1. Shattering a two point set asks for a member meeting it in the first point alone and a member meeting it in the second point alone; whichever of the two members is contained in the other already contains its own point, so it meets the set in both. This is why the extremal families fordedare families of cuts: the number of cuts is exactly what a chain in a linear order can achieve.∀ {α : Type u_2} {𝒜 : Set (Set α)}, IsChain (fun x1 x2 => x1 ⊆ x2) 𝒜 → HasVCDimLE 1 𝒜 - Declded'_eq_dedDeclaration kindtheorem
The convention question is empty at infinite cardinals:
dedandded'agree there. It is not empty in general, byded'_one_lt_ded_one.∀ {κ : Cardinal.{u}}, Cardinal.aleph0 ≤ κ → ded' κ = ded κUsed by
- Declded_le_ded'Declaration kindtheorem
The two readings of "dense subset" define the same cardinal function at every infinite cardinal. Every bracketing witness is turned into a strict witness of at least its size by
mk_le_ded'_of_isDenseIn, at the cost of a countable factor in the dense subset, which an infiniteκabsorbs.∀ {κ : Cardinal.{u}}, Cardinal.aleph0 ≤ κ → ded κ ≤ ded' κUsed by
- Declmk_le_ded'_of_isDenseInDeclaration kindtheorem
∀ {κ : Cardinal.{u}} {J : Type u} [inst : LinearOrder J] {E : Set J}, Cardinal.aleph0 ≤ κ → Cardinal.mk ↑E ≤ κ → IsDenseIn E → Cardinal.mk J ≤ ded' κUsed by
- Declmk_le_mk_fattenDeclaration kindtheorem
∀ {J : Type u} (E : Set J), Cardinal.mk J ≤ Cardinal.mk ↑(fatten✝ E)Used by
- Declfatten_bot_injectiveDeclaration kindtheorem
∀ {J : Type u} (E : Set J), Function.Injective fun x => ⟨toLex (x, 0), ⋯⟩Used by
- Declmk_le_ded'Declaration kindtheorem
The defining property of
ded': a linear order with a strictly dense subset of size at mostκhas at mostded' κpoints.∀ {κ : Cardinal.{u}} {J : Type u} [inst : LinearOrder J] {E : Set J}, Cardinal.mk ↑E ≤ κ → IsStrictlyDenseIn E → Cardinal.mk J ≤ ded' κUses
Used by
- DeclbddAbove_dedSet'Declaration kindtheorem
∀ (κ : Cardinal.{u}), BddAbove (dedSet'✝ κ)Uses
Used by
- DecldedSet'_leDeclaration kindtheorem
∀ {κ c : Cardinal.{u}}, c ∈ dedSet'✝ κ → c ≤ 2 ^ (κ + κ)Used by
- Declmk_fattenDense_leDeclaration kindtheorem
∀ {J : Type u} (E : Set J), Cardinal.mk ↑(fattenDense✝ E) ≤ Cardinal.mk ↑E * Cardinal.aleph0Used by
- DeclfattenDense_code_injectiveDeclaration kindtheorem
∀ {J : Type u} (E : Set J), Function.Injective fun p => (⟨(ofLex ↑↑p).1, ⋯⟩, (ofLex ↑↑p).2)Used by
- DeclisStrictlyDenseIn_fattenDenseDeclaration kindtheorem
∀ {J : Type u} [inst : LinearOrder J] {E : Set J}, IsDenseIn E → IsStrictlyDenseIn (fattenDense✝ E)Used by
- Declexists_strictly_between_fattenDeclaration kindtheorem
The heart of the comparison: in the blow-up, every pair is separated strictly by a point lying over
E. The three cases of the bracketing witnessdarea < d < b, where the fibre overdsupplies the point;d = a, where the point is taken higher in the fibre overa; andd = b, where it is taken lower in the fibre overb.∀ {J : Type u} [inst : LinearOrder J] {E : Set J}, IsDenseIn E → ∀ {u v : Lex (J × ℚ)}, u ∈ fatten✝ E → v ∈ fatten✝ E → u < v → ∃ z ∈ E, ∃ r, u < toLex (z, r) ∧ toLex (z, r) < v - Declmem_of_fatten_of_fst_eqDeclaration kindtheorem
∀ {J : Type u} {E : Set J} {u v : Lex (J × ℚ)}, u ∈ fatten✝ E → v ∈ fatten✝ E → (ofLex u).1 = (ofLex v).1 → (ofLex u).2 < (ofLex v).2 → (ofLex u).1 ∈ E - Declded_leDeclaration kindtheorem
The elimination rule for
ded.∀ {κ c : Cardinal.{u}}, (∀ (J : Type u) (x : LinearOrder J) (E : Set J), Cardinal.mk ↑E ≤ κ → IsDenseIn E → Cardinal.mk J ≤ c) → ded κ ≤ cUsed by
- Declded'_le_dedDeclaration kindtheorem
Strict density is the stronger condition on the subset, so fewer orders are witnesses and the supremum is no larger. This holds at every cardinal.
∀ (κ : Cardinal.{u}), ded' κ ≤ ded κUsed by
- Declmk_le_dedDeclaration kindtheorem
The defining property of
ded, in the form used downstream: a linear order with a dense subset of size at mostκhas at mostded κpoints.∀ {κ : Cardinal.{u}} {J : Type u} [inst : LinearOrder J] {E : Set J}, Cardinal.mk ↑E ≤ κ → IsDenseIn E → Cardinal.mk J ≤ ded κUses
Used by
- DeclbddAbove_dedSetDeclaration kindtheorem
∀ (κ : Cardinal.{u}), BddAbove (dedSet✝ κ)Uses
Used by
- DecldedSet_leDeclaration kindtheorem
∀ {κ c : Cardinal.{u}}, c ∈ dedSet✝ κ → c ≤ 2 ^ (κ + κ)Used by
- DeclIsDenseIn.mk_le_two_pow_mulDeclaration kindtheorem
A linear order with a dense subset
Dhas at most2 ^ #D * 2 ^ #Dpoints, since a point is determined by the pair of cuts it induces onD.∀ {J : Type u} [inst : LinearOrder J] {E : Set J}, IsDenseIn E → Cardinal.mk J ≤ 2 ^ Cardinal.mk ↑E * 2 ^ Cardinal.mk ↑EUsed by
- DeclcutCode_injectiveDeclaration kindtheorem
∀ {I : Type u_1} {D : Set I} [inst : LinearOrder I], IsDenseIn D → Function.Injective (cutCode✝ D)Uses
Used by
- DeclcutCode_neDeclaration kindtheorem
∀ {I : Type u_1} {D : Set I} [inst : LinearOrder I], IsDenseIn D → ∀ {x y : I}, x < y → cutCode✝ D x ≠ cutCode✝ D yUsed by
- Declded'_leDeclaration kindtheorem
The elimination rule for
ded'.∀ {κ c : Cardinal.{u}}, (∀ (J : Type u) (x : LinearOrder J) (E : Set J), Cardinal.mk ↑E ≤ κ → IsStrictlyDenseIn E → Cardinal.mk J ≤ c) → ded' κ ≤ cUsed by
- DeclIsStrictlyDenseIn.isDenseInDeclaration kindtheorem
∀ {I : Type u_1} {D : Set I} [inst : Preorder I], IsStrictlyDenseIn D → IsDenseIn DUsed by
- Hypothesishκ
Cardinal.aleph0 ≤ κ
- Hypothesish
lam < ded κ
A set family
𝒜has VC dimension at mostdif all the sets it shatters have size at mostd.{α : Type u_1} → ℕ → Set (Set α) → Prop- DefinitionIsDenseIndef
Dis dense in a preorderIwhen every paira < bbrackets a point ofD, that is, when there isd ∈ Dwitha ≤ d ≤ b. On a linear order without jumps this agrees with strict betweenness; on an order with jumps it is strictly weaker, and it is the form under whichdedbounds the size of the order.{I : Type u_1} → [Preorder I] → Set I → Prop - DefinitionIsStrictlyDenseIndef
Dis strictly dense in a preorderIwhen every paira < bhas a point ofDstrictly between them. This is the second of the two readings of "dense subset" that the definition ofdedin the literature leaves open; the first isIsDenseIn. Where the order has no jumps the two agree, and a linear order with a jump whose two endpoints lie inDsatisfiesIsDenseInonly. The literature ondeddoes not say which reading is meant;ded'_eq_dedshows the question does not affect the value ofdedat an infinite cardinal.{I : Type u_1} → [Preorder I] → Set I → Prop 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- DefinitioncutCodedef
The pair of cuts a point of
Iinduces onD.{I : Type u_1} → [Preorder I] → (D : Set I) → I → Set ↑D × Set ↑D - Definitiondeddef
ded κis the supremum of the cardinalities of the linear orders that admit a dense subset of size at mostκ. The supremum is taken over a set of cardinals bounded above by2 ^ (κ + κ), so it is not a junk value. Carriers are restricted toType u, which does not move the supremum, every witness having size at most2 ^ (κ + κ).Cardinal.{u} → Cardinal.{u} - Definitionded'def
ded' κis the supremum of the cardinalities of the linear orders that admit a strictly dense subset of size at mostκ. It is the same construction asded, with strict betweenness in place of bracketing, and is bounded above by the same2 ^ (κ + κ).Cardinal.{u} → Cardinal.{u} - DefinitiondedSetdef
The set of cardinalities of linear orders with a dense subset of size at most
κ.Cardinal.{u} → Set Cardinal.{u} - DefinitiondedSet'def
The set of cardinalities of linear orders with a strictly dense subset of size at most
κ.Cardinal.{u} → Set Cardinal.{u} - Definitionfattendef
The blow-up of
JalongE: the lexicographic productJ ×ₗ ℚwith the fibre over each point outsideEcollapsed to the single rational0.{J : Type u} → Set J → Set (Lex (J × ℚ)) - DefinitionfattenDensedef
The part of the blow-up lying over
E, that is, the union of the fullℚfibres.{J : Type u} → (E : Set J) → Set ↑(fatten✝ E) - DefinitionpadCutsdef
The witness family: the down sets of
J, carried into the padded ground type.(J P : Type u) → [LinearOrder J] → Set (Set (J ⊕ P))
- DefinitionpadGrounddef
The ground set of the witness: a subset
EofJtogether with a disjoint copy ofP, whose points no member of the family below meets.{J P : Type u} → Set J → Set (J ⊕ P)
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
- 6089d733e525
- Verified
- 2026-09-24T00:00:00Z