weaklyRegular — Mathlib

English

A regular measure on an R1-space is weakly regular.

Русский

Регулярная мера на пространстве R1 имеет слабую регулярность.

LaTeX

$$$[R1Space\ \alpha] \ [Regular\ \mu] \Rightarrow \mu\text{ is WeaklyRegular}.$$$

Lean4

/-- A regular measure is weakly regular in an R₁ space. -/
instance (priority := 100) weaklyRegular [R1Space α] [Regular μ] : WeaklyRegular μ where
  innerRegular := fun _U hU r hr ↦
    let ⟨K, KU, K_comp, hK⟩ := Regular.innerRegular hU r hr
    ⟨closure K, K_comp.closure_subset_of_isOpen hU KU, isClosed_closure, hK.trans_le (measure_mono subset_closure)⟩

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