Documentation

LeanPool.LanguageGeneration.FiniteWitness.Width.Value

The ordered range 0,1,2,...,omega,omega+1, and its exact threshold.

source
@[reducible, inline]
abbrev GenLimit.FiniteWitness.SeparationValue :
Type

The ordered width values 0, 1, 2, ..., omega, and omega+1.

Equations
Instances For
    source
    def GenLimit.FiniteWitness.finiteValue (n : ℕ) :
    SeparationValue

    Embed a finite witness bound into the separation-width range.

    Equations
    Instances For
      source
      def GenLimit.FiniteWitness.omegaValue :
      SeparationValue

      The width value for finite witnesses with no uniform finite bound.

      Equations
      Instances For
        source
        @[simp]
        theorem GenLimit.FiniteWitness.finiteValue_le_iff (m n : ℕ) :
        finiteValue m ≤ finiteValue n ↔ m ≤ n
        source
        @[simp]
        theorem GenLimit.FiniteWitness.finiteValue_le_omega (n : ℕ) :
        finiteValue n ≤ omegaValue
        source
        @[simp]
        theorem GenLimit.FiniteWitness.not_omega_le_finite (n : ℕ) :
        ¬omegaValue ≤ finiteValue n
        source
        @[simp]
        theorem GenLimit.FiniteWitness.omega_ne_top :
        omegaValue ≠ ⊤
        source
        @[simp]
        theorem GenLimit.FiniteWitness.finiteValue_ne_top (n : ℕ) :
        finiteValue n ≠ ⊤
        source
        @[simp]
        theorem GenLimit.FiniteWitness.finiteValue_ne_omega (n : ℕ) :
        finiteValue n ≠ omegaValue
        source
        noncomputable def GenLimit.FiniteWitness.separationWidth {α : Type u_1} (H : Set (Set α)) :
        SeparationValue

        A convenient normal form for the optimized width. The accompanying minimum theorem identifies it with the paper's assignment-cost definition.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem GenLimit.FiniteWitness.HasBoundedWitnesses.hasFiniteWitnesses {α : Type u_1} {H : Set (Set α)} {d : ℕ} (h : HasBoundedWitnesses H d) :
          HasFiniteWitnesses H
          source
          theorem GenLimit.FiniteWitness.finiteWitnesses_mono {α : Type u_1} {H K : Set (Set α)} (h : HasFiniteWitnesses H) (hKH : K ⊆ H) :
          HasFiniteWitnesses K
          source
          theorem GenLimit.FiniteWitness.width_le_finite_iff {α : Type u_1} (H : Set (Set α)) (d : ℕ) :
          separationWidth H ≤ finiteValue d ↔ HasBoundedWitnesses H d
          source
          theorem GenLimit.FiniteWitness.width_le_omega_iff {α : Type u_1} (H : Set (Set α)) :
          separationWidth H ≤ omegaValue ↔ HasFiniteWitnesses H
          source
          theorem GenLimit.FiniteWitness.ordinary_iff_width {α : Type u_1} [Countable α] [Infinite α] (H : Set (Set α)) (hUUS : Generic.UUS H) :
          Generic.GeneratableInLimit H ↔ separationWidth H ≤ omegaValue
          source
          theorem GenLimit.FiniteWitness.width_eq_omega_iff {α : Type u_1} (H : Set (Set α)) :
          separationWidth H = omegaValue ↔ HasFiniteWitnesses H ∧ ∀ (d : ℕ), ¬HasBoundedWitnesses H d
          source
          theorem GenLimit.FiniteWitness.width_eq_top_iff {α : Type u_1} (H : Set (Set α)) :
          separationWidth H = ⊤ ↔ ¬HasFiniteWitnesses H
          source
          theorem GenLimit.FiniteWitness.width_mono {α : Type u_1} {H K : Set (Set α)} (hHK : H ⊆ K) :
          separationWidth H ≤ separationWidth K
          source
          theorem GenLimit.FiniteWitness.bounded_zero_iff_core_infinite {α : Type u_1} [Infinite α] (H : Set (Set α)) :
          HasBoundedWitnesses H 0 ↔ (⋂₀ H).Infinite
          source
          theorem GenLimit.FiniteWitness.width_zero_iff {α : Type u_1} [Infinite α] (H : Set (Set α)) :
          separationWidth H = finiteValue 0 ↔ (⋂₀ H).Infinite