innerRegularWRT_isCompact_isClosed

English

For μ, InnerRegularWRT (IsCompact s ∧ IsClosed s) IsClosed is equivalent to InnerRegularWRT IsCompact IsClosed.

Русский

Для μ внутренняя регулярность по ((IsCompact s) ∧ IsClosed s) эквивалентна внутренней регулярности по IsCompact и IsClosed.

LaTeX

$$$\\mu.InnerRegularWRT (\\lambda s. IsCompact\\,s \\land IsClosed\\,s) IsClosed \\iff \\mu.InnerRegularWRT IsCompact IsClosed.$$$

Lean4

theorem innerRegularWRT_isCompact_isClosed [UniformSpace α] [CompleteSpace α] [SecondCountableTopology α]
    [(uniformity α).IsCountablyGenerated] [OpensMeasurableSpace α] (P : Measure α) [IsFiniteMeasure P] :
    P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed :=
  by
  rw [innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure]
  exact innerRegularWRT_isCompact_closure P

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