innerRegularWRT_isCompact_isClosed_iff

English

The inner regularity with respect to compact and closed sets is equivalent to the inner regularity with respect to compact and closed sets after closure.

Русский

Внутренняя регулярность по компактным и замкнутым множествам эквивалентна внутренней регулярности после замыкания.

LaTeX

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

Lean4

theorem innerRegularWRT_isCompact_isClosed_iff [TopologicalSpace α] [R1Space α] :
    μ.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) IsClosed ↔ μ.InnerRegularWRT IsCompact IsClosed :=
  innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure.trans innerRegularWRT_isCompact_closure_iff

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