Documentation

LeanPool.LanguageGeneration.FiniteWitness.Width.TwoCore

An explicit family with finite witnesses of unbounded size #

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

The two-copy universe shared with the anchored hierarchy examples.

Equations
Instances For
    source
    def GenLimit.FiniteWitness.TwoCore.HasLeft (L : Set Point) :
    Prop

    A language contains the entire left copy of the natural numbers.

    Equations
    Instances For
      source
      def GenLimit.FiniteWitness.TwoCore.HasRight (L : Set Point) :
      Prop

      A language contains the entire right copy of the natural numbers.

      Equations
      Instances For
        source
        def GenLimit.FiniteWitness.TwoCore.family :
        Set (Set Point)

        The languages containing at least one of the two infinite copies.

        Equations
        Instances For
          source
          def GenLimit.FiniteWitness.TwoCore.leftTarget (D : Set ℕ) :
          Set Point

          A full left copy together with an arbitrary subset of the right copy.

          Equations
          Instances For
            source
            def GenLimit.FiniteWitness.TwoCore.rightTarget (E : Set ℕ) :
            Set Point

            A full right copy together with an arbitrary subset of the left copy.

            Equations
            Instances For
              source
              @[simp]
              theorem GenLimit.FiniteWitness.TwoCore.inl_left (D : Set ℕ) (n : ℕ) :
              Sum.inl n ∈ leftTarget D
              source
              @[simp]
              theorem GenLimit.FiniteWitness.TwoCore.inr_right (E : Set ℕ) (n : ℕ) :
              Sum.inr n ∈ rightTarget E
              source
              @[simp]
              theorem GenLimit.FiniteWitness.TwoCore.inr_left (D : Set ℕ) (n : ℕ) :
              Sum.inr n ∈ leftTarget D ↔ n ∈ D
              source
              @[simp]
              theorem GenLimit.FiniteWitness.TwoCore.inl_right (E : Set ℕ) (n : ℕ) :
              Sum.inl n ∈ rightTarget E ↔ n ∈ E
              source
              theorem GenLimit.FiniteWitness.TwoCore.left_mem (D : Set ℕ) :
              leftTarget D ∈ family
              source
              theorem GenLimit.FiniteWitness.TwoCore.right_mem (E : Set ℕ) :
              rightTarget E ∈ family
              source
              theorem GenLimit.FiniteWitness.TwoCore.family_uus :
              Generic.UUS family
              source
              noncomputable def GenLimit.FiniteWitness.TwoCore.assignment (L : Set Point) :
              Finset Point

              Witness a missing point in one copy by a finite initial segment of the other copy.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem GenLimit.FiniteWitness.TwoCore.assignment_positive :
                Positive family assignment
                source
                theorem GenLimit.FiniteWitness.TwoCore.no_cross {L K : Set Point} :
                HasLeft L → ∀ (hR : HasRight K) (hnR : ¬HasRight L) (hnL : ¬HasLeft K), ¬(↑(assignment L) ⊆ K ∧ ↑(assignment K) ⊆ L)
                source
                theorem GenLimit.FiniteWitness.TwoCore.assignment_valid :
                Valid family assignment
                source
                theorem GenLimit.FiniteWitness.TwoCore.anchored_subset (k : ℕ) :
                Anchored.family k ⊆ family
                source
                theorem GenLimit.FiniteWitness.TwoCore.no_finite_bound (d : ℕ) :
                ¬HasBoundedWitnesses family d
                source
                theorem GenLimit.FiniteWitness.TwoCore.exact_width :
                separationWidth family = omegaValue
                source
                theorem GenLimit.FiniteWitness.TwoCore.ordinary :
                Generic.GeneratableInLimit family