Cardinal bounds

On infinite ground sets, the exact bound on traces is Dedekind's ded.

• MTH.C-2026-6007HasVCDimLE.mk_image_inter_le_ded

  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.

• MTH.C-2026-6008no_smaller_bound

  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.