English
For any set function m: Set α → ℝ≥0∞, there exists a unique maximal outer measure μ that satisfies μ(s) ≤ m(s) for all sets s, given by μ = OuterMeasure.ofFunction (λ s, ⨆_{s.Nonempty} m s) with the default zero-value on the empty set. This outer measure is often called the maximal outer measure bounded by m.
Русский
Для любой функции m: Set α → ℝ≥0∞ существует единственная максимальная внешняя мера μ, удовлетворяющая μ(s) ≤ m(s) для всякого множества s; μ задаётся как OuterMeasure.ofFunction (λ s, ⨆_{s≠∅} m s) с дефолтным нулём на пустом множестве. Такая внешняя мера называется максимальной, ограниченной m.
LaTeX
$$$ \\text{boundedBy } m = \\mathrm{OuterMeasure.ofFunction}(\\lambda s, \\; \\big\\lbrace \\!\\!\\!\\!\\!\\!\\!\\!⨆ _ : s.Nonempty, m s\\big\\rbrace)\\; (\\text{with } m_{\\emptyset}=0 \\text{ as the default})$$$
Lean4
/-- Given any function `m` assigning measures to sets, there is a unique maximal outer measure `μ`
satisfying `μ s ≤ m s` for all `s : Set α`. This is the same as `OuterMeasure.ofFunction`,
except that it doesn't require `m ∅ = 0`. -/
def boundedBy : OuterMeasure α :=
OuterMeasure.ofFunction (fun s => ⨆ _ : s.Nonempty, m s) (by simp [Set.not_nonempty_empty])
