Mathesis

Dhruv GuptaZetetic-Dhruvperson2026-09-24T00:00:00Z

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 by Dhruv Gupta

ThesisStepHypothesisDefinition

DeclHasVCDimLE.mk_image_inter_le_dedDeclaration kindtheorem

∀ {α : Type u} {𝒜 : Set (Set α)} {A : Set α} {d : ℕ},
  HasVCDimLE d 𝒜 → A.Infinite → Cardinal.mk ↑((fun x => A ∩ x) '' 𝒜) ≤ ded (Cardinal.mk ↑A)

HasVCDimLE Shatters ded

Uses

exists_shatters_of_ded_lt_mk_image_inter

Declexists_shatters_of_ded_lt_mk_image_interDeclaration kindtheorem
Shelah's theorem. A family that traces more than ded #A sets on an infinite ground set A shatters finite subsets of A of every size. The proof takes a subset B ⊆ A of least cardinality on which the family still traces more than ded #A sets, enumerates B by an initial ordinal so that every proper initial segment is smaller than B and therefore carries at most ded #A traces, prunes the tree of traces along that enumeration to the nodes at least (ded #A)⁺ members pass through, and walks down the pruned tree collecting one point per step.
The conclusion cannot be strengthened to an infinite shattered set: the finite subsets of ℕ shatter every finite set and no infinite one.
The statement is due to Shelah. Both expositions used here, Adler, Introduction to theories without the independence property, Theorem 23, and Simon, A Guide to NIP Theories, Proposition 2.69, state it for the space of complete φ-types over a parameter set rather than for a set family, and the reading under which a complete φ-type over A is a trace on A and the independence property is the shattering of arbitrarily large finite sets is the standard translation of that statement, not a form either source asserts.
```
∀ {α : Type u} {𝒜 : Set (Set α)} {A : Set α},
  A.Infinite →
    ded (Cardinal.mk ↑A) < Cardinal.mk ↑((fun x => A ∩ x) '' 𝒜) →
      ∀ (n : ℕ), ∃ S ⊆ A, S.Finite ∧ S.ncard = n ∧ Shatters 𝒜 S
```
Shatters ded
Uses
Used by
- HasVCDimLE.mk_image_inter_le_ded
Declmk_Iio_lt_ordDeclaration kindtheorem
```
∀ {ν : Cardinal.{u}} (w : ν.ord.ToType), Cardinal.mk ↑(Set.Iio w) < ν
```
Used by
- exists_shatters_of_ded_lt_mk_image_inter
Declexists_shatter_tuple_of_enumDeclaration kindtheorem
Shelah's argument in the tree language: an enumeration of a ground set of size μ all of whose initial segments carry at most θ traces, with ded μ ≤ θ and more than θ traces on the whole set, yields for each n a set of n indices on which 𝒜 cuts out every pattern. The ceiling θ⁺ is regular, so the pruning of mk_sdiff_core_lt applies and the core keeps the whole width.
```
∀ {α : Type u} {𝒜 : Set (Set α)} {W : Type u} {e : W → α} [inst : LinearOrder W] [WellFoundedLT W] {μ θ : Cardinal.{u}},
  Cardinal.aleph0 ≤ μ →
    Cardinal.mk W = μ →
      Cardinal.aleph0 ≤ θ →
        ded μ ≤ θ →
          (∀ (w : W), Cardinal.mk ↑((fun x => e '' Set.Iic w ∩ x) '' 𝒜) ≤ θ) →
            θ < Cardinal.mk ↑((fun x => Set.range e ∩ x) '' 𝒜) →
              ∀ (n : ℕ), ∃ S, S.Finite ∧ S.ncard = n ∧ ∀ (σ : Set W), ∃ C ∈ 𝒜, ∀ x ∈ S, e x ∈ C ↔ x ∈ σ
```
big bigAt core ded enc truncate valIn valOut
Uses
Used by
- exists_shatters_of_ded_lt_mk_image_inter
Declself_le_dedDeclaration kindtheorem
```
∀ (κ : Cardinal.{u}), κ ≤ ded κ
```
ded dedSet
Uses
- bddAbove_dedSet
- self_mem_dedSet
Used by
- exists_shatter_tuple_of_enum
- exists_shatters_of_ded_lt_mk_image_inter
Declmk_truncate_image_enc_imageDeclaration kindtheorem
The level-w nodes of the tree of codes are the traces on the initial segment e '' Iic w.
```
∀ {α : Type u} {𝒜 : Set (Set α)} {W : Type u} {e : W → α} [inst : LinearOrder W] (w : W),
  Cardinal.mk ↑(truncate w '' enc✝ e '' 𝒜) = Cardinal.mk ↑((fun x => e '' Set.Iic w ∩ x) '' 𝒜)
```
enc truncate
Uses
Used by
- exists_shatter_tuple_of_enum

Decltruncate_enc_eq_iffDeclaration kindtheorem

∀ {α W : Type u} {e : W → α} {C C' : Set α} [inst : LinearOrder W] {w : W},
  truncate w (enc✝ e C) = truncate w (enc✝ e C') ↔ ∀ v ≤ w, e v ∈ C ↔ e v ∈ C'

enc truncate

Uses

enc_apply_eq_iff
truncate_apply

Used by

mk_truncate_image_enc_image

Declmk_sdiff_core_ltDeclaration kindtheorem
Pruning to the core costs fewer than lam members: a member outside the core has a narrow truncation, the narrow nodes at one level are fewer than lam and carry fewer than lam members each, and there are fewer than lam levels. Regularity of lam closes both sums.
```
∀ {W : Type u} [inst : LinearOrder W] {β : Type u} [inst_1 : LinearOrder β] [inst_2 : OrderBot β]
  {F : Set (Lex (W → β))} {lam : Cardinal.{u}},
  lam.IsRegular →
    Cardinal.mk W < lam → (∀ (w : W), Cardinal.mk ↑(truncate w '' F) < lam) → Cardinal.mk ↑(F \ core✝ lam F) < lam
```
big bigAt core truncate
Used by
- exists_shatter_tuple_of_enum
Declmk_image_inter_range_le_mk_enc_imageDeclaration kindtheorem
The traces on the range of e are at most as many as the codes along e, two members with the same code agreeing at every index.
```
∀ {α : Type u} {𝒜 : Set (Set α)} {W : Type u} {e : W → α},
  Cardinal.mk ↑((fun x => Set.range e ∩ x) '' 𝒜) ≤ Cardinal.mk ↑(enc✝ e '' 𝒜)
```
enc
Uses
Used by
- exists_shatter_tuple_of_enum
Declmk_image_le_mk_imageDeclaration kindtheorem
If g separates at most as much as f does on s, then f '' s is no larger than g '' s.
```
∀ {β γ δ : Type u} {s : Set β} {f : β → γ} {g : β → δ},
  (∀ x ∈ s, ∀ y ∈ s, g x = g y → f x = f y) → Cardinal.mk ↑(f '' s) ≤ Cardinal.mk ↑(g '' s)
```
Used by
- mk_image_inter_range_le_mk_enc_image
- mk_truncate_image_enc_image
Declinter_eq_inter_iffDeclaration kindtheorem
```
∀ {α : Type u} {C C' D : Set α}, D ∩ C = D ∩ C' ↔ ∀ a ∈ D, a ∈ C ↔ a ∈ C'
```
Used by
- mk_image_inter_range_le_mk_enc_image
- mk_truncate_image_enc_image

Declenc_eq_iffDeclaration kindtheorem

∀ {α W : Type u} {e : W → α} {C C' : Set α}, enc✝ e C = enc✝ e C' ↔ ∀ (w : W), e w ∈ C ↔ e w ∈ C'

enc

Uses

enc_apply_eq_iff

Used by

mk_image_inter_range_le_mk_enc_image

Declenc_apply_eq_iffDeclaration kindtheorem

∀ {α W : Type u} {e : W → α} {C C' : Set α} {w : W}, ofLex (enc✝ e C) w = ofLex (enc✝ e C') w ↔ (e w ∈ C ↔ e w ∈ C')

enc valIn valOut

Uses

enc_apply
valIn_ne_valOut

Used by

enc_eq_iff
truncate_enc_eq_iff

Declexists_shatter_tupleDeclaration kindtheorem
The induction that produces the shattered points. In a two-valued tree whose core is wide, every wide node carries, for each n, a set of n indices above its own level on which the members of F below it realise every pattern. The step spends the wide node: lt_mk_big_fiber gives more than μ wide nodes below it, exists_level concentrates them on one level, the pigeonhole on finite index sets returns two of them with a common tuple, and the index where the two disagree is the new point. Its position, strictly above the old level and at or below the new one, is what keeps the points distinct. This is the combinatorial form of the claim proved by induction in Adler, Theorem 23, and in Simon, Proposition 2.69.
```
∀ {W : Type u} [inst : LinearOrder W] [WellFoundedLT W] {F : Set (Lex (W → WithBot (ULift.{u, 0} Bool)))}
  {μ lam : Cardinal.{u}},
  Cardinal.aleph0 ≤ μ →
    Cardinal.mk W = μ →
      lam.IsRegular →
        Cardinal.mk ↑(F \ core✝ lam F) < lam →
          ded μ < lam →
            (∀ g ∈ F, ∀ (x : W), ofLex g x = valIn✝ ∨ ofLex g x = valOut✝) →
              ∀ (n : ℕ) (w : W),
                ∀ p ∈ bigAt✝ lam F w,
                  ∃ S,
                    S.Finite ∧
                      S.ncard = n ∧
                        (∀ x ∈ S, w < x) ∧
                          ∀ (σ : Set W), ∃ g ∈ F, truncate w g = p ∧ ∀ x ∈ S, ofLex g x = valIn✝ ↔ x ∈ σ
```
bigAt core ded truncate valIn valOut
Uses
Used by
- exists_shatter_tuple_of_enum

Declval_of_mem_image_truncateDeclaration kindtheorem

A node inherits two-valuedness from the members it truncates.

∀ {W : Type u} [inst : LinearOrder W] {F : Set (Lex (W → WithBot (ULift.{u, 0} Bool)))}
  {q : Lex (W → WithBot (ULift.{u, 0} Bool))} {x v : W},
  (∀ g ∈ F, ∀ (y : W), ofLex g y = valIn✝ ∨ ofLex g y = valOut✝) →
    q ∈ truncate v '' F → x ≤ v → ofLex q x = valIn✝ ∨ ofLex q x = valOut✝

truncate valIn valOut

Uses

ofLex_truncate_of_le

Used by

exists_shatter_tuple

DeclofLex_truncate_of_leDeclaration kindtheorem

Below the level of truncation the sequence is unchanged.

∀ {W : Type u} [inst : LinearOrder W] {β : Type u} [inst_1 : LinearOrder β] [inst_2 : OrderBot β] {v : W}
  {g : Lex (W → β)} {x : W}, x ≤ v → ofLex (truncate v g) x = ofLex g x

truncate

Uses

truncate_apply

Used by

exists_shatter_tuple
val_of_mem_image_truncate

Declmk_setOf_finite_ncard_leDeclaration kindtheorem
The finite subsets of an infinite W of a prescribed size are at most #W many. This is the pigeonhole that forces two nodes at one level to carry the same tuple.
```
∀ {W : Type u}, Cardinal.aleph0 ≤ Cardinal.mk W → ∀ (n : ℕ), Cardinal.mk ↑{S | S.Finite ∧ S.ncard = n} ≤ Cardinal.mk W
```
Used by
- exists_shatter_tuple

Decllt_of_mk_ltDeclaration kindtheorem

The level found by exists_level lies strictly above the node's own level: at or below it the fibre is a single node, hence too small.

∀ {W : Type u} [inst : LinearOrder W] {β : Type u} [inst_1 : LinearOrder β] [inst_2 : OrderBot β]
  {F : Set (Lex (W → β))} {lam μ : Cardinal.{u}} {v w : W} {p : Lex (W → β)},
  Cardinal.aleph0 ≤ μ → μ < Cardinal.mk ↑{q | q ∈ bigAt✝ lam F v ∧ truncate w q = p} → w < v

bigAt truncate

Uses

truncate_truncate

Used by

exists_shatter_tuple

Decllt_mk_big_fiberDeclaration kindtheorem
The step at which ded enters the argument. Below a wide node p, the core members extending p are at least lam many, and they form a set of branches whose nodes are the wide nodes extending p together with the truncations of p itself. The tree bound therefore caps them by ded of that node set, so if the wide nodes extending p were at most μ the count would be at most ded (μ + #W), which is below lam.
```
∀ {W : Type u} [inst : LinearOrder W] {β : Type u} [inst_1 : LinearOrder β] [inst_2 : OrderBot β]
  {F : Set (Lex (W → β))} {lam μ : Cardinal.{u}} {w : W} {p : Lex (W → β)} [WellFoundedLT W],
  lam.IsRegular →
    Cardinal.mk ↑(F \ core✝ lam F) < lam →
      p ∈ bigAt✝ lam F w → ded (μ + Cardinal.mk W) < lam → μ < Cardinal.mk ↑{q | q ∈ big✝ lam F ∧ truncate w q = p}
```
big bigAt core ded truncate
Uses
Used by
- exists_shatter_tuple

Decltruncate_truncateDeclaration kindtheorem

∀ {W : Type u} [inst : LinearOrder W] {β : Type u} [inst_1 : LinearOrder β] [inst_2 : OrderBot β] (w v : W)
  (b : Lex (W → β)), truncate w (truncate v b) = truncate (min w v) b

truncate

Used by

exists_shatter_tuple
lt_mk_big_fiber
lt_of_mk_lt

Declmk_le_ded_of_truncate_memDeclaration kindtheorem
The tree bound: a set 𝒮 of sequences all of whose truncations lie in 𝒟 has at most ded #𝒟 elements. Equivalently, a tree with at most κ nodes has at most ded κ branches. The order is taken on 𝒮 ∪ 𝒟 with 𝒟 as the dense subset: given f < g there, either g lies in 𝒟 and brackets the pair by itself, or g lies in 𝒮 and the truncation of g at the first index where f and g differ lies between them.
```
∀ {W : Type u} [inst : LinearOrder W] {β : Type u} [inst_1 : LinearOrder β] [inst_2 : OrderBot β] [WellFoundedLT W]
  {𝒮 𝒟 : Set (Lex (W → β))} {κ : Cardinal.{u}},
  (∀ f ∈ 𝒮, ∀ (w : W), truncate w f ∈ 𝒟) → Cardinal.mk ↑𝒟 ≤ κ → Cardinal.mk ↑𝒮 ≤ ded κ
```
ded truncate
Uses
Used by
- lt_mk_big_fiber

Decltruncate_leDeclaration kindtheorem

∀ {W : Type u} [inst : LinearOrder W] {β : Type u} [inst_1 : LinearOrder β] [inst_2 : OrderBot β] [WellFoundedLT W]
  (w : W) (b : Lex (W → β)), truncate w b ≤ b

truncate

Uses

lex_lt_iff
truncate_apply

Used by

mk_le_ded_of_truncate_mem

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 most ded κ points.
```
∀ {κ : Cardinal.{u}} {J : Type u} [inst : LinearOrder J] {E : Set J},
  Cardinal.mk ↑E ≤ κ → IsDenseIn E → Cardinal.mk J ≤ ded κ
```
IsDenseIn ded dedSet
Uses
- bddAbove_dedSet
Used by
- mk_le_ded_of_truncate_mem

Decllt_truncateDeclaration kindtheorem

∀ {W : Type u} [inst : LinearOrder W] {β : Type u} [inst_1 : LinearOrder β] [inst_2 : OrderBot β] {a b : Lex (W → β)}
  {w : W}, (∀ j < w, ofLex a j = ofLex b j) → ofLex a w < ofLex b w → a < truncate w b

truncate

Uses

lex_lt_iff
truncate_apply

Used by

mk_le_ded_of_truncate_mem

Decltruncate_applyDeclaration kindtheorem

∀ {W : Type u} [inst : LinearOrder W] {β : Type u} [inst_1 : LinearOrder β] [inst_2 : OrderBot β] (w : W)
  (b : Lex (W → β)) (v : W), ofLex (truncate w b) v = if v ≤ w then ofLex b v else ⊥

truncate

Used by

exists_shatter_tuple
lt_truncate
ofLex_truncate_of_le
truncate_enc_eq_iff
truncate_le

Decllex_lt_iffDeclaration kindtheorem

∀ {W : Type u} [inst : LinearOrder W] {β : Type u} [inst_1 : LinearOrder β] {a b : Lex (W → β)},
  a < b ↔ ∃ i, (∀ j < i, ofLex a j = ofLex b j) ∧ ofLex a i < ofLex b i

Used by

lt_truncate
mk_le_ded_of_truncate_mem
truncate_le

Declle_mk_core_fiberDeclaration kindtheorem

A wide node stays wide inside the core, the pruning having removed fewer than lam members.

∀ {W : Type u} [inst : LinearOrder W] {β : Type u} [inst_1 : LinearOrder β] [inst_2 : OrderBot β]
  {F : Set (Lex (W → β))} {lam : Cardinal.{u}} {w : W} {p : Lex (W → β)},
  lam.IsRegular →
    Cardinal.mk ↑(F \ core✝ lam F) < lam →
      p ∈ bigAt✝ lam F w → lam ≤ Cardinal.mk ↑{g | g ∈ core✝ lam F ∧ truncate w g = p}

bigAt core truncate

Used by

lt_mk_big_fiber

Declexists_levelDeclaration kindtheorem

The wide nodes below a fixed node spread over the levels, so if they are more than μ in total and the levels are at most μ, one level already carries more than μ of them.

∀ {W : Type u} [inst : LinearOrder W] {β : Type u} [inst_1 : LinearOrder β] [inst_2 : OrderBot β]
  {F : Set (Lex (W → β))} {lam μ : Cardinal.{u}} {w : W} {p : Lex (W → β)},
  Cardinal.aleph0 ≤ μ →
    Cardinal.mk W ≤ μ →
      μ < Cardinal.mk ↑{q | q ∈ big✝ lam F ∧ truncate w q = p} →
        ∃ v, μ < Cardinal.mk ↑{q | q ∈ bigAt✝ lam F v ∧ truncate w q = p}

big bigAt truncate

Used by

exists_shatter_tuple

Declenc_apply_eq_valIn_orDeclaration kindtheorem

∀ {α W : Type u} {e : W → α} (C : Set α) (w : W), ofLex (enc✝ e C) w = valIn✝ ∨ ofLex (enc✝ e C) w = valOut✝

enc valIn valOut

Uses

enc_apply

Used by

exists_shatter_tuple_of_enum

Declenc_apply_eq_valIn_iffDeclaration kindtheorem
```
∀ {α W : Type u} {e : W → α} (C : Set α) (w : W), ofLex (enc✝ e C) w = valIn✝ ↔ e w ∈ C
```
enc valIn valOut
Uses
- enc_apply
- valIn_ne_valOut
Used by
- exists_shatter_tuple_of_enum
DeclvalIn_ne_valOutDeclaration kindtheorem
```
valIn✝ ≠ valOut✝
```
valIn valOut
Used by

Declenc_applyDeclaration kindtheorem

∀ {α W : Type u} {e : W → α} {C : Set α} (w : W), ofLex (enc✝ e C) w = if e w ∈ C then valIn✝ else valOut✝

enc valIn valOut

Used by

enc_apply_eq_iff
enc_apply_eq_valIn_iff
enc_apply_eq_valIn_or

Declexists_minimal_subsetDeclaration kindtheorem
The reduction that makes the tree small. Among the subsets of A whose trace family outruns θ there is one of least cardinality, Cardinal being well-ordered. Along an enumeration of that subset every proper initial segment carries at most θ traces, which is what the tree bound needs and what a well-order of A itself does not supply.
```
∀ {α : Type u} {𝒜 : Set (Set α)} {A : Set α} {θ : Cardinal.{u}},
  θ < Cardinal.mk ↑((fun x => A ∩ x) '' 𝒜) →
    ∃ B ⊆ A,
      θ < Cardinal.mk ↑((fun x => B ∩ x) '' 𝒜) ∧
        ∀ B' ⊆ A, Cardinal.mk ↑B' < Cardinal.mk ↑B → Cardinal.mk ↑((fun x => B' ∩ x) '' 𝒜) ≤ θ
```
Used by
- exists_shatters_of_ded_lt_mk_image_inter
Declded_le_dedDeclaration kindtheorem
```
∀ {κ₁ κ₂ : Cardinal.{u}}, κ₁ ≤ κ₂ → ded κ₁ ≤ ded κ₂
```
IsDenseIn ded dedSet
Uses
- bddAbove_dedSet
- self_mem_dedSet
Used by
- exists_shatters_of_ded_lt_mk_image_inter
Declself_mem_dedSetDeclaration kindtheorem
```
∀ (κ : Cardinal.{u}), κ ∈ dedSet✝ κ
```
IsDenseIn dedSet
Uses
- isDenseIn_univ
Used by
- ded_le_ded
- self_le_ded
DeclisDenseIn_univDeclaration kindtheorem
```
∀ {I : Type u_1} [inst : Preorder I], IsDenseIn Set.univ
```
IsDenseIn
Used by
- self_mem_dedSet
DeclbddAbove_dedSetDeclaration kindtheorem
```
∀ (κ : Cardinal.{u}), BddAbove (dedSet✝ κ)
```
dedSet
Uses
- dedSet_le
Used by
DecldedSet_leDeclaration kindtheorem
```
∀ {κ c : Cardinal.{u}}, c ∈ dedSet✝ κ → c ≤ 2 ^ (κ + κ)
```
IsDenseIn dedSet
Uses
- IsDenseIn.mk_le_two_pow_mul
Used by
- bddAbove_dedSet
DeclIsDenseIn.mk_le_two_pow_mulDeclaration kindtheorem
A linear order with a dense subset D has at most 2 ^ #D * 2 ^ #D points, since a point is determined by the pair of cuts it induces on D.
```
∀ {J : Type u} [inst : LinearOrder J] {E : Set J}, IsDenseIn E → Cardinal.mk J ≤ 2 ^ Cardinal.mk ↑E * 2 ^ Cardinal.mk ↑E
```
IsDenseIn cutCode
Uses
- cutCode_injective
Used by
- dedSet_le
DeclcutCode_injectiveDeclaration kindtheorem
```
∀ {I : Type u_1} {D : Set I} [inst : LinearOrder I], IsDenseIn D → Function.Injective (cutCode✝ D)
```
IsDenseIn cutCode
Uses
- cutCode_ne
Used by
- IsDenseIn.mk_le_two_pow_mul

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 y

IsDenseIn cutCode

Used by

cutCode_injective

Hypothesish𝒜
```
HasVCDimLE d 𝒜
```
HypothesishA
```
A.Infinite
```
DefinitionHasVCDimLEdefYaël Dillies
A set family 𝒜 has VC dimension at most d if all the sets it shatters have size at most d.
```
{α : Type u_1} → ℕ → Set (Set α) → Prop
```
DefinitionIsDenseIndef
D is dense in a preorder I when every pair a < b brackets a point of D, that is, when there is d ∈ D with a ≤ 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 which ded bounds the size of the order.
```
{I : Type u_1} → [Preorder I] → Set I → Prop
```
DefinitionShattersdefYaël Dillies
A set family 𝒜 shatters a set A if all subsets of A can be obtained as the intersection of A with some element of the set family. We also say that A is traced by 𝒜.
```
{α : Type u_1} → [SemilatticeInf α] → Set α → α → Prop
```

Definitionbigdef

The wide nodes of the tree of truncations of F, at all levels.

{W : Type u} →
  [LinearOrder W] →
    {β : Type u} → [inst : LinearOrder β] → [OrderBot β] → Cardinal.{u} → Set (Lex (W → β)) → Set (Lex (W → β))

DefinitionbigAtdef

The level-w truncations of F that at least lam members of F extend.

{W : Type u} →
  [LinearOrder W] →
    {β : Type u} → [inst : LinearOrder β] → [OrderBot β] → Cardinal.{u} → Set (Lex (W → β)) → W → Set (Lex (W → β))

Definitioncoredef

The members of F all of whose truncations are wide.

{W : Type u} →
  [LinearOrder W] →
    {β : Type u} → [inst : LinearOrder β] → [OrderBot β] → Cardinal.{u} → Set (Lex (W → β)) → Set (Lex (W → β))

DefinitioncutCodedef

The pair of cuts a point of I induces on D.

{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 by 2 ^ (κ + κ), so it is not a junk value. Carriers are restricted to Type u, which does not move the supremum, every witness having size at most 2 ^ (κ + κ).
```
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}
```

Definitionencdef

The code of C along an indexing e of the ground set.

{α W : Type u} → (W → α) → Set α → Lex (W → WithBot (ULift.{u, 0} Bool))

Definitiontruncatedef

The sequence agreeing with b up to w and equal to ⊥ above it.

{W : Type u} → [LinearOrder W] → {β : Type u} → [inst : LinearOrder β] → [OrderBot β] → W → Lex (W → β) → Lex (W → β)

DefinitionvalIndef
The two defined values of the alphabet coding a partial trace; ⊥ marks the positions where the trace is undefined.
```
WithBot (ULift.{u, 0} Bool)
```
DefinitionvalOutdef
```
WithBot (ULift.{u, 0} Bool)
```

DOIMTH.R-2026-6007

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: 7f14a7125689
Verified: 2026-09-24T00:00:00Z