innerRegularWRT_isCompact_closure

English

If p is preserved under intersections with q and μ(K^c) can be made arbitrarily small when K satisfies p, then μ has inner regularity with respect to p and q.

Русский

Если p сохраняется при пересечении с q, и μ(K^c) может быть сделана сколь угодно малой, когда K удовлетворяет p, тогда μ регулярен по p и q.

LaTeX

$$$\\forall A,B\\, (pA \\land qB \\Rightarrow p(A\\cap B)) \\land (\\forall ε>0, ∃ K, pK ∧ μ(K^c) < ε) \\Rightarrow μ.InnerRegularWRT p q.$$$

Lean4

theorem innerRegularWRT_isCompact_closure [UniformSpace α] [CompleteSpace α] [SecondCountableTopology α]
    [(uniformity α).IsCountablyGenerated] [OpensMeasurableSpace α] (P : Measure α) [IsFiniteMeasure P] :
    P.InnerRegularWRT (IsCompact ∘ closure) IsClosed :=
  innerRegularWRT_isCompact_closure_of_univ (exists_isCompact_closure_measure_compl_lt P)

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