Endpoint examples and realization of the entire width range

def GenLimit.FiniteWitness.allInfinite (α : Type u_2) : Set (Set α)

The family of all infinite subsets of a universe.

Equations

• GenLimit.FiniteWitness.allInfinite α = {L : Set α | L.Infinite}

def GenLimit.FiniteWitness.cofinite (α : Type u_2) : Set (Set α)

The family of subsets with finite complement.

Equations

• GenLimit.FiniteWitness.cofinite α = {L : Set α | Lᶜ.Finite}

theorem GenLimit.FiniteWitness.allInfinite_uus {α : Type u_1} : Generic.UUS (allInfinite α)

theorem GenLimit.FiniteWitness.cofinite_uus {α : Type u_1} [Infinite α] : Generic.UUS (cofinite α)

theorem GenLimit.FiniteWitness.cofinite_subset_allInfinite {α : Type u_1} [Infinite α] : cofinite α ⊆ allInfinite α

theorem GenLimit.FiniteWitness.cofinite_countable {α : Type u_1} [Countable α] : (cofinite α).Countable

theorem GenLimit.FiniteWitness.cofinite_core_empty {α : Type u_1} : ⋂₀ cofinite α = ∅

theorem GenLimit.FiniteWitness.cofinite_width {α : Type u_1} [Countable α] [Infinite α] : separationWidth (cofinite α) = finiteValue 1

theorem GenLimit.FiniteWitness.allInfinite_no_finiteWitnesses {α : Type u_1} [Countable α] [Infinite α] : ¬HasFiniteWitnesses (allInfinite α)

theorem GenLimit.FiniteWitness.allInfinite_width {α : Type u_1} [Countable α] [Infinite α] : separationWidth (allInfinite α) = ⊤

theorem GenLimit.FiniteWitness.cofinite_ordinary {α : Type u_1} [Countable α] [Infinite α] : Generic.GeneratableInLimit (cofinite α)

theorem GenLimit.FiniteWitness.allInfinite_not_ordinary {α : Type u_1} [Countable α] [Infinite α] : ¬Generic.GeneratableInLimit (allInfinite α)

theorem GenLimit.FiniteWitness.full_range_on_sum (v : SeparationValue) : ∃ (H : Set (Set TwoCore.Point)), Generic.UUS H ∧ separationWidth H = v

theorem GenLimit.FiniteWitness.full_range {α : Type u_1} [Countable α] [Infinite α] (v : SeparationValue) : ∃ (H : Set (Set α)), Generic.UUS H ∧ separationWidth H = v