GreedyOpenSelection.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Countable selection of compatible open barriers

A basis enumeration selects one admissible candidate at each finite stage. If removing previous candidates allows a candidate with the same or larger open set, every candidate admissible for the final family has its open set covered by that family. This is the selection step only; countability of unavailable ends is separate.

def OAI.CircleDomainRigidity.greedyStep line 26
theorem OAI.CircleDomainRigidity.greedyStep_contains line 31
theorem OAI.CircleDomainRigidity.greedyStep_finite line 40
theorem OAI.CircleDomainRigidity.greedyStep_new_subsingleton line 49

theorem OAI.CircleDomainRigidity.exists_countable_open_selection line 62

Source documentation

Select a countable compatible family whose union covers every finally admissible candidate. The stage condition retains the actual order of selection.

theorem exists_countable_open_selection [TopologicalSpace X] [SecondCountableTopology X]
    (U : C → Set X) (hU : ∀ c, IsOpen (U c))
    (Allowed : Set C → C → Prop)
    (hrestrict : ∀ {A D : Set C}, A ⊆ D → ∀ c, Allowed D c →
      ∃ d, Allowed A d ∧ U c ⊆ U d) :
    ∃ A : ℕ → Set C,
      A 0 = ∅ ∧ (∀ n, (A n).Finite) ∧ Monotone A ∧
      (∀ n, (A (n + 1) \ A n).Subsingleton) ∧
      (∀ n c, c ∈ A (n + 1) \ A n → Allowed (A n) c) ∧
      (⋃ n, A n).Countable ∧
      ∀ c, Allowed (⋃ n, A n) c → U c ⊆ ⋃ d ∈ ⋃ n, A n, U d := by
…

theorem OAI.CircleDomainRigidity.exists_countable_graded_open_selection line 105

Source documentation

The open-set selection can impose every countably indexed accuracy demand at once, retaining compatibility across different accuracies.

theorem exists_countable_graded_open_selection
    [TopologicalSpace X] [SecondCountableTopology X]
    (U : C → Set X) (hU : ∀ c, IsOpen (U c)) (grade : C → ℕ)
    (Allowed : Set C → C → Prop)
    (hrestrict : ∀ {A D : Set C}, A ⊆ D → ∀ c, Allowed D c →
      ∃ d, Allowed A d ∧ grade d = grade c ∧ U c ⊆ U d) :
    ∃ A : ℕ → Set C,
      A 0 = ∅ ∧ (∀ n, (A n).Finite) ∧ Monotone A ∧
      (∀ n, (A (n + 1) \ A n).Subsingleton) ∧
      (∀ n c, c ∈ A (n + 1) \ A n → Allowed (A n) c) ∧
      (⋃ n, A n).Countable ∧
      ∀ c, Allowed (⋃ n, A n) c → ∀ x ∈ U c,
…

theorem OAI.CircleDomainRigidity.exists_countable_graded_cover line 136

Source documentation

If only countably many endpoints lack an admissible test at each accuracy, the graded selection leaves only countably many endpoints uncovered. The hypothesis is precisely where the separate path-law argument is needed.

theorem exists_countable_graded_cover
    [TopologicalSpace X] [SecondCountableTopology X]
    (U : C → Set X) (hU : ∀ c, IsOpen (U c)) (grade : C → ℕ)
    (Allowed : Set C → C → Prop)
    (hrestrict : ∀ {A D : Set C}, A ⊆ D → ∀ c, Allowed D c →
      ∃ d, Allowed A d ∧ grade d = grade c ∧ U c ⊆ U d)
    (hunavailable : ∀ A : Set C, A.Countable → ∀ k : ℕ,
      {x | ¬∃ c, Allowed A c ∧ grade c = k ∧ x ∈ U c}.Countable) :
    ∃ A : ℕ → Set C,
      A 0 = ∅ ∧ (∀ n, (A n).Finite) ∧ Monotone A ∧
      (∀ n, (A (n + 1) \ A n).Subsingleton) ∧
      (∀ n c, c ∈ A (n + 1) \ A n → Allowed (A n) c) ∧
…