Compactness Time Exhaustion

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.exists_compact_exhaustion_of_open_real (I : Set ℝ) (hI : IsOpen I) : ∃ (J : ℕ → Set ℝ), (∀ (n : ℕ), IsCompact (J n)) ∧ (∀ (n : ℕ), J n ⊆ I) ∧ (∀ (n : ℕ), J n ⊆ J (n + 1)) ∧ (∀ (n : ℕ), J n ⊆ interior (J (n + 1))) ∧ ⋃ (n : ℕ), J n = I

A compact exhaustion of an open time domain by ambient compact sets.

theorem CKN.Leray.compact_time_subset_eventually_in_exhaustion {I T : Set ℝ} (hT : IsCompact T) (hTI : T ⊆ I) (J : ℕ → Set ℝ) (hmono : ∀ (j : ℕ), J j ⊆ J (j + 1)) (hinner : ∀ (j : ℕ), J j ⊆ interior (J (j + 1))) (hcover : ⋃ (j : ℕ), J j = I) : ∃ (j : ℕ), T ⊆ J j

A compact subset of an open time domain lies in one sufficiently large member of a nested compact exhaustion.

theorem CKN.Leray.compact_time_subset_compact_interval {I T : Set ℝ} (hI : I.OrdConnected) (hT : IsCompact T) (hTI : T ⊆ I) : ∃ (a : ℝ) (b : ℝ), T ⊆ Set.Icc a b ∧ Set.Icc a b ⊆ I

A compact time set inside an interval fits inside a compact interval contained in the same domain.