innerRegularWRT_isCompact_isOpen — Mathlib

English

If a measure P is regular, then P is inner regular with respect to IsCompact and IsOpen.

Русский

Если мера P регулярна, то она внутренняя регулярна по IsCompact и IsOpen.

LaTeX

$$$\\text{Regular}(P) \\Rightarrow P.InnerRegularWRT IsCompact IsOpen.$$$

Lean4

theorem innerRegularWRT_isCompact_isOpen [PseudoEMetricSpace α] [CompleteSpace α] [SecondCountableTopology α]
    [OpensMeasurableSpace α] (P : Measure α) [IsFiniteMeasure P] : P.InnerRegularWRT IsCompact IsOpen :=
  (innerRegularWRT_isCompact P).trans (Measure.InnerRegularWRT.of_pseudoMetrizableSpace P)

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