innerRegularWRT_isClosed_isOpen — Mathlib

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)⟩

Похожие утверждения