An infinitary positive-separation characterization

A single positive assignment must separate every subfamily with finite full intersection. The subfamilies here are arbitrary sets of languages. This file extends, and does not alter, the previously checked characterization.

def GenLimit.FiniteWitness.Separates {α : Type u_1} (H : Generic.LanguageClass α) (T : Generic.Language α → Finset α) : Prop

Every finite-core subfamily contains a witness point missing from a member.

Equations

• GenLimit.FiniteWitness.Separates H T = ∀ F ⊆ H, F.Nonempty → (⋂₀ F).Finite → ∃ L ∈ F, ∃ K ∈ F, ∃ x ∈ T L, x ∉ K

theorem GenLimit.FiniteWitness.finiteWitnesses_iff_separating {α : Type u_1} (H : Generic.LanguageClass α) : HasFiniteWitnesses H ↔ ∃ (T : Generic.Language α → Finset α), (∀ L ∈ H, ↑(T L) ⊆ L) ∧ Separates H T

The full finite-witness criterion equals simultaneous positive separation.

theorem GenLimit.FiniteWitness.ordinary_iff_separating {α : Type u_1} [Countable α] [Infinite α] (H : Generic.LanguageClass α) (hUUS : Generic.UUS H) : Generic.GeneratableInLimit H ↔ ∃ (T : Generic.Language α → Finset α), (∀ L ∈ H, ↑(T L) ⊆ L) ∧ Separates H T

Ordinary generation is equivalent to finitely supported positive separation.