outerRegular — Mathlib

English

If μ admits finite spanning open sets with outer regular restrictions, then μ is outer regular.

Русский

Если μ допускает конечные открытые покрытия, для которых ограничение внешне регулярно, то μ внешне регулярна.

LaTeX

$$$OuterRegular(μ) \leftarrow (s: μ.FiniteSpanningSetsIn\{U\mid IsOpen U \land OuterRegular(μ.restrict U)\})$$$

Lean4

/-- If a measure `μ` admits finite spanning open sets such that the restriction of `μ` to each set
is outer regular, then the original measure is outer regular as well. -/
protected theorem outerRegular [TopologicalSpace α] [OpensMeasurableSpace α] {μ : Measure α}
    (s : μ.FiniteSpanningSetsIn {U | IsOpen U ∧ OuterRegular (μ.restrict U)}) : OuterRegular μ :=
  OuterRegular.of_restrict (s := fun n ↦ s.set n) (fun n ↦ (s.set_mem n).2) (fun n ↦ (s.set_mem n).1)
    s.spanning.symm.subset

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