Set-valued separators and their cardinality cost

def GenLimit.FiniteWitness.IsSeparator {α : Type u_1} (H : Set (Set α)) (P : Set α → Set α) : Prop

A positive set-valued assignment that separates every subfamily with finite intersection.

Equations

• GenLimit.FiniteWitness.IsSeparator H P = ((∀ L ∈ H, P L ⊆ L) ∧ GenLimit.FiniteWitness.SetSeparates H P)

noncomputable def GenLimit.FiniteWitness.setCost {α : Type u_1} (S : Set α) : SeparationValue

The finite cardinality of a set, or the top width value for an infinite set.

Equations

• GenLimit.FiniteWitness.setCost S = if h : S.Finite then GenLimit.FiniteWitness.finiteValue h.toFinset.card else ⊤

noncomputable def GenLimit.FiniteWitness.assignmentCost {α : Type u_1} (H : Set (Set α)) (P : Set α → Set α) : SeparationValue

The supremum of the assigned set costs over the target family.

Equations

• GenLimit.FiniteWitness.assignmentCost H P = ⨆ (L : ↑H), GenLimit.FiniteWitness.setCost (P ↑L)

theorem GenLimit.FiniteWitness.setCost_le_finite_iff {α : Type u_1} (S : Set α) (d : ℕ) : setCost S ≤ finiteValue d ↔ ∃ (h : S.Finite), h.toFinset.card ≤ d

theorem GenLimit.FiniteWitness.setCost_le_omega_iff {α : Type u_1} (S : Set α) : setCost S ≤ omegaValue ↔ S.Finite

theorem GenLimit.FiniteWitness.cost_le_finite_iff {α : Type u_1} (H : Set (Set α)) (P : Set α → Set α) (d : ℕ) : assignmentCost H P ≤ finiteValue d ↔ ∀ L ∈ H, ∃ (h : (P L).Finite), h.toFinset.card ≤ d

theorem GenLimit.FiniteWitness.cost_le_omega_iff {α : Type u_1} (H : Set (Set α)) (P : Set α → Set α) : assignmentCost H P ≤ omegaValue ↔ ∀ L ∈ H, (P L).Finite

theorem GenLimit.FiniteWitness.separator_to_valid {α : Type u_1} {H : Set (Set α)} {P : Set α → Set α} (hP : IsSeparator H P) (hf : ∀ L ∈ H, (P L).Finite) : ∃ (T : Set α → Finset α), Valid H T ∧ ∀ L ∈ H, ↑(T L) = P L

theorem GenLimit.FiniteWitness.valid_to_separator {α : Type u_1} {H : Set (Set α)} {T : Set α → Finset α} (h : Valid H T) : IsSeparator H fun (L : Set α) => ↑(T L)

theorem GenLimit.FiniteWitness.bounded_iff_cost_le {α : Type u_1} (H : Set (Set α)) (d : ℕ) : HasBoundedWitnesses H d ↔ ∃ (P : Set α → Set α), IsSeparator H P ∧ assignmentCost H P ≤ finiteValue d

theorem GenLimit.FiniteWitness.finiteWitnesses_iff_cost_le_omega {α : Type u_1} (H : Set (Set α)) : HasFiniteWitnesses H ↔ ∃ (P : Set α → Set α), IsSeparator H P ∧ assignmentCost H P ≤ omegaValue

theorem GenLimit.FiniteWitness.identity_separator {α : Type u_1} {H : Set (Set α)} (hUUS : Generic.UUS H) : IsSeparator H id

theorem GenLimit.FiniteWitness.width_le_assignmentCost {α : Type u_1} {H : Set (Set α)} {P : Set α → Set α} (hP : IsSeparator H P) : separationWidth H ≤ assignmentCost H P

theorem GenLimit.FiniteWitness.width_cost_attained {α : Type u_1} {H : Set (Set α)} (hUUS : Generic.UUS H) : ∃ (P : Set α → Set α), IsSeparator H P ∧ assignmentCost H P = separationWidth H

theorem GenLimit.FiniteWitness.width_isLeast_cost {α : Type u_1} {H : Set (Set α)} (hUUS : Generic.UUS H) : IsLeast {w : SeparationValue | ∃ (P : Set α → Set α), IsSeparator H P ∧ assignmentCost H P = w} (separationWidth H)

Exact correspondence with the minimum-over-assignments definition in the paper.

theorem GenLimit.FiniteWitness.width_eq_finite_of_bounds {α : Type u_1} {H : Set (Set α)} {d : ℕ} (hu : HasBoundedWitnesses H d) (hl : ∀ (q : ℕ), HasBoundedWitnesses H q → d ≤ q) : separationWidth H = finiteValue d