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