Pressure Gradient Origin Cell Instance Exhaustion

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

def CKN.Core.Step4.OriginInstance.exhaustionCore (I : Set ℝ) (n : ℕ) : Set ℝ

The points of the closed interval [-n, n] whose closed 1/(n+1)-ball lies in I.

Equations

• CKN.Core.Step4.OriginInstance.exhaustionCore I n = Set.Icc (-↑n) ↑n ∩ {t : ℝ | Metric.closedBall t (1 / (↑n + 1)) ⊆ I}

theorem CKN.Core.Step4.OriginInstance.exists_compact_ordConnected_exhaustion {I : Set ℝ} (hopen : IsOpen I) (hord : I.OrdConnected) : ∃ (J : ℕ → Set ℝ), Monotone J ∧ (∀ (n : ℕ), (J n).OrdConnected) ∧ (∀ (n : ℕ), IsCompact (J n)) ∧ (∀ (n : ℕ), J n ⊆ I) ∧ ⋃ (n : ℕ), J n = I ∧ ∀ (T : Set ℝ), IsCompact T → T ⊆ I → ∃ (n : ℕ), T ⊆ J n

An open, order-connected subset of the line is the increasing union of compact order-connected subsets, and every compact subset is contained in one of them.