Eventually unbounded positive closure and bounded witnesses

def GenLimit.FiniteWitness.EventuallyUnboundedClosure {α : Type u_1} (H : Set (Set α)) : Prop

Each target contains a finite sample with infinite positive closure.

Equations

• GenLimit.FiniteWitness.EventuallyUnboundedClosure H = ∀ L ∈ H, ∃ (F : Finset α), ↑F ⊆ L ∧ (GenLimit.FiniteWitness.positiveClosure H F).Infinite

theorem GenLimit.FiniteWitness.positiveClosure_mono_sample {α : Type u_1} {H : Set (Set α)} {F S : Finset α} (hFS : F ⊆ S) : positiveClosure H F ⊆ positiveClosure H S

theorem GenLimit.FiniteWitness.euc_uus {α : Type u_1} {H : Set (Set α)} (hH : EventuallyUnboundedClosure H) : Generic.UUS H

theorem GenLimit.FiniteWitness.euc_iff_eventual_on_texts {α : Type u_1} [Countable α] (H : Set (Set α)) (hUUS : Generic.UUS H) : EventuallyUnboundedClosure H ↔ ∀ L ∈ H, ∀ (stream : Generic.Stream α), Generic.Presents stream L → ∃ (N : ℕ), ∀ n ≥ N, (positiveClosure H (Generic.sample stream n)).Infinite

theorem GenLimit.FiniteWitness.increasing_euc_cover {α : Type u_1} {H : Set (Set α)} (K : ℕ → Set (Set α)) (hmono : Monotone K) (hcover : H = ⋃ (n : ℕ), K n) (hEUC : ∀ (n : ℕ), EventuallyUnboundedClosure (K n)) : HasFiniteWitnesses H

The increasing cover is only a sufficient condition; necessity is not asserted.

theorem GenLimit.FiniteWitness.increasing_euc_cover_ordinary {α : Type u_1} [Countable α] [Infinite α] {H : Set (Set α)} (K : ℕ → Set (Set α)) (hmono : Monotone K) (hcover : H = ⋃ (n : ℕ), K n) (hEUC : ∀ (n : ℕ), EventuallyUnboundedClosure (K n)) : Generic.GeneratableInLimit H