innerRegularWRT_isCompact_isClosed_isOpen

English

A measure regularity with respect to the predicate IsCompact ∧ IsClosed implies regularity with respect to IsOpen when the space is suitable.

Русский

Регулярность по предикату IsCompact ∧ IsClosed переходит в регулярность по IsOpen на подходящем пространстве.

LaTeX

$$$\\text{InnerRegularWRT }(\\text{IsCompact} \\land \\text{IsClosed}) \\text{IsOpen}$$$

Lean4

theorem innerRegularWRT_isCompact_isClosed_isOpen [PseudoEMetricSpace α] [CompleteSpace α] [SecondCountableTopology α]
    [OpensMeasurableSpace α] (P : Measure α) [IsFiniteMeasure P] :
    P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsOpen :=
  (innerRegularWRT_isCompact_isClosed P).trans (Measure.InnerRegularWRT.of_pseudoMetrizableSpace P)

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