English
Every open set U can be written as a union of an increasing sequence of closed sets F_n with F_n ⊆ U for all n.
Русский
Каждое открытое множество U можно выразить как объединение возрастающей последовательности замкнутых множеств F_n, причём F_n ⊆ U для всех n.
LaTeX
$$$\exists F: \mathbb{N} \to \text{Set}(\alpha),\ (\forall n, \text{IsClosed}(F(n))) \land (\forall n, F(n) \subseteq U) \land (\bigcup_n F(n) = U) \land (\text{Monotone}(F))$$$
Lean4
theorem _root_.IsOpen.exists_iUnion_isClosed {U : Set α} (hU : IsOpen U) :
∃ F : ℕ → Set α, (∀ n, IsClosed (F n)) ∧ (∀ n, F n ⊆ U) ∧ ⋃ n, F n = U ∧ Monotone F :=
by
obtain ⟨a, a_pos, a_lt_one⟩ : ∃ a : ℝ≥0∞, 0 < a ∧ a < 1 := exists_between zero_lt_one
let F := fun n : ℕ => (fun x => infEdist x Uᶜ) ⁻¹' Ici (a ^ n)
have F_subset : ∀ n, F n ⊆ U := fun n x hx ↦ by
by_contra h
have : infEdist x Uᶜ ≠ 0 := ((ENNReal.pow_pos a_pos _).trans_le hx).ne'
exact this (infEdist_zero_of_mem h)
refine ⟨F, fun n => IsClosed.preimage continuous_infEdist isClosed_Ici, F_subset, ?_, ?_⟩
· show ⋃ n, F n = U
refine Subset.antisymm (by simp only [iUnion_subset_iff, F_subset, forall_const]) fun x hx => ?_
have : x ∉ Uᶜ := by simpa using hx
rw [mem_iff_infEdist_zero_of_closed hU.isClosed_compl] at this
have B : 0 < infEdist x Uᶜ := by simpa [pos_iff_ne_zero] using this
have : Filter.Tendsto (fun n => a ^ n) atTop (𝓝 0) := ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one a_lt_one
rcases ((tendsto_order.1 this).2 _ B).exists with ⟨n, hn⟩
simp only [mem_iUnion]
exact ⟨n, hn.le⟩
show Monotone F
intro m n hmn x hx
simp only [F, mem_Ici, mem_preimage] at hx ⊢
apply le_trans (pow_le_pow_right_of_le_one' a_lt_one.le hmn) hx
