Fixed-assignment interfaces and arbitrary positive separating sets.

def GenLimit.FiniteWitness.Positive {α : Type u_1} (H : Set (Set α)) (T : Set α → Finset α) : Prop

Every assigned witness consists of positive examples from its target language.

Equations

• GenLimit.FiniteWitness.Positive H T = ∀ L ∈ H, ↑(T L) ⊆ L

def GenLimit.FiniteWitness.Valid {α : Type u_1} (H : Set (Set α)) (T : Set α → Finset α) : Prop

A positive witness assignment whose nonempty active subfamilies have infinite common cores.

Equations

• One or more equations did not get rendered due to their size.

def GenLimit.FiniteWitness.HasBoundedWitnesses {α : Type u_1} (H : Set (Set α)) (d : ℕ) : Prop

Existence of a valid witness assignment with a uniform finite cardinality bound.

Equations

• GenLimit.FiniteWitness.HasBoundedWitnesses H d = ∃ (T : Set α → Finset α), GenLimit.FiniteWitness.Valid H T ∧ ∀ L ∈ H, (T L).card ≤ d

theorem GenLimit.FiniteWitness.valid_iff_positive_separates {α : Type u_1} (H : Set (Set α)) (T : Set α → Finset α) : Valid H T ↔ Positive H T ∧ Separates H T

theorem GenLimit.FiniteWitness.Valid.hasFiniteWitnesses {α : Type u_1} {H : Set (Set α)} {T : Set α → Finset α} (h : Valid H T) : HasFiniteWitnesses H

theorem GenLimit.FiniteWitness.Valid.mono {α : Type u_1} {H K : Set (Set α)} {T : Set α → Finset α} (h : Valid H T) (hKH : K ⊆ H) : Valid K T

theorem GenLimit.FiniteWitness.HasBoundedWitnesses.mono {α : Type u_1} {H K : Set (Set α)} {d : ℕ} (h : HasBoundedWitnesses H d) (hKH : K ⊆ H) : HasBoundedWitnesses K d

theorem GenLimit.FiniteWitness.HasBoundedWitnesses.mono_bound {α : Type u_1} {H : Set (Set α)} {d e : ℕ} (h : HasBoundedWitnesses H d) (hde : d ≤ e) : HasBoundedWitnesses H e

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

Every nonempty subfamily with finite intersection contains targets separated by an assigned set.

Equations

• GenLimit.FiniteWitness.SetSeparates H P = ∀ F ⊆ H, F.Nonempty → (⋂₀ F).Finite → ∃ L ∈ F, ∃ K ∈ F, ¬P L ⊆ K

theorem GenLimit.FiniteWitness.setSeparates_finset {α : Type u_1} (H : Set (Set α)) (T : Set α → Finset α) : (SetSeparates H fun (L : Set α) => ↑(T L)) ↔ Separates H T

theorem GenLimit.FiniteWitness.exists_countable_same_core {α : Type u_1} [Countable α] {F : Set (Set α)} (hF : F.Nonempty) : ∃ C ⊆ F, C.Nonempty ∧ C.Countable ∧ ⋂₀ C = ⋂₀ F

theorem GenLimit.FiniteWitness.setSeparates_iff_countable {α : Type u_1} [Countable α] (H : Set (Set α)) (P : Set α → Set α) : SetSeparates H P ↔ ∀ F ⊆ H, F.Nonempty → F.Countable → (⋂₀ F).Finite → ∃ L ∈ F, ∃ K ∈ F, ¬P L ⊆ K