English
If α is an R1-space with an opens-measurable σ-algebra and μ is inner regular, then μ is inner regular with respect to IsClosed and IsOpen; i.e., closed sets approximate via inner regularity against open sets.
Русский
Если пространство — R1, сигма-алгебра измеримых открытых множеств, и μ — внутренняя регулярность, то μ сохраняет регулярность по замкнутым и открытым множествам.
LaTeX
$$$[R1Space\\ α]\\; [OpensMeasurableSpace\\ α]\\; [h: InnerRegular μ] \\Rightarrow InnerRegularWRT μ IsClosed IsOpen$$$
Lean4
theorem innerRegularWRT_isClosed_isOpen [R1Space α] [OpensMeasurableSpace α] [h : InnerRegular μ] :
InnerRegularWRT μ IsClosed IsOpen := by
intro U hU r hr
rcases h.innerRegular hU.measurableSet r hr with ⟨K, KU, K_comp, hK⟩
exact ⟨closure K, K_comp.closure_subset_of_isOpen hU KU, isClosed_closure, hK.trans_le (measure_mono subset_closure)⟩