Singleton witnesses for countable language families

theorem GenLimit.FiniteWitness.exists_injective_choice_avoiding {α : Type u_1} (A : ℕ → Set α) (hA : ∀ (n : ℕ), (A n).Infinite) (B : ℕ → Finset α) : ∃ (p : ℕ → α), Function.Injective p ∧ ∀ (n : ℕ), p n ∈ A n ∧ p n ∉ B n

noncomputable def GenLimit.FiniteWitness.finiteCoreForbidden {α : Type u_1} (V : Finset (Set α)) : Finset α

The union of the finite intersections of subfamilies of a finite language family.

Equations

• GenLimit.FiniteWitness.finiteCoreForbidden V = V.powerset.biUnion fun (F : Finset (Set α)) => if h : (⋂₀ ↑F).Finite then h.toFinset else ∅

theorem GenLimit.FiniteWitness.mem_finiteCoreForbidden {α : Type u_1} {V : Finset (Set α)} {F : Set (Set α)} (hF : F.Finite) (hFV : F ⊆ ↑V) (hC : (⋂₀ F).Finite) {x : α} (hx : x ∈ ⋂₀ F) : x ∈ finiteCoreForbidden V

theorem GenLimit.FiniteWitness.countable_singleton_witnesses {α : Type u_1} [Infinite α] {H : Set (Set α)} (hH : H.Countable) (hUUS : Generic.UUS H) : ∃ (p : ↑H → α), Function.Injective p ∧ ∃ (T : Set α → Finset α), Valid H T ∧ ∀ (L : ↑H), T ↑L = {p L}

theorem GenLimit.FiniteWitness.countable_hasBoundedWitnesses_one {α : Type u_1} [Infinite α] {H : Set (Set α)} (hH : H.Countable) (hUUS : Generic.UUS H) : HasBoundedWitnesses H 1

theorem GenLimit.FiniteWitness.countable_ordinary {α : Type u_1} [Infinite α] {H : Set (Set α)} (hH : H.Countable) (hUUS : Generic.UUS H) : Generic.GeneratableInLimit H