English
In a metrizable (or pseudo-metrizable) space, any open set can be approximated from inside by a sequence of closed sets. More precisely, if μ is inner regular with respect to closed sets and open sets, then for every open set U there exists a sequence of closed sets F_n ⊆ U with μ(U) = sup_n μ(F_n).
Русский
В метризуемом (или псевдометрическом) пространстве каждое открытое множество может быть аппроксимировано изнутри последовательностью замкнутых множеств F_n ⊆ U, причём μ(U) равно наибольшей верхней границе μ(F_n).
LaTeX
$$$\\forall U\\,(Open\\,U)\\;\\exists (F_n)_{n∈\\mathbb{N}}:\\; (\\forall n\\, F_n \\subseteq U) \\land IsClosed F_n\\land μ(U) = \\sup_n μ(F_n)$$$
Lean4
/-- In a metrizable space (or even a pseudo metrizable space), an open set can be approximated from
inside by closed sets. -/
theorem of_pseudoMetrizableSpace {X : Type*} [TopologicalSpace X] [PseudoMetrizableSpace X] [MeasurableSpace X]
(μ : Measure X) : InnerRegularWRT μ IsClosed IsOpen :=
by
let A : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
intro U hU r hr
rcases hU.exists_iUnion_isClosed with ⟨F, F_closed, -, rfl, F_mono⟩
rw [F_mono.measure_iUnion] at hr
rcases lt_iSup_iff.1 hr with ⟨n, hn⟩
exact ⟨F n, subset_iUnion _ _, F_closed n, hn⟩
