English
sInfGen m s is defined as the infimum of μ(s) over all μ in m.
Русский
sInfGen m s определяется как инфимуум по μ(s) для всех μ из множества m.
LaTeX
$$$\\mathrm{sInfGen}\, m\\, s = \\inf_{\\mu} \\{\\mu(s) : \\mu \\in m\\}$$$
Lean4
/-- Given a set of outer measures, we define a new function that on a set `s` is defined to be the
infimum of `μ(s)` for the outer measures `μ` in the collection. We ensure that this
function is defined to be `0` on `∅`, even if the collection of outer measures is empty.
The outer measure generated by this function is the infimum of the given outer measures. -/
def sInfGen (m : Set (OuterMeasure α)) (s : Set α) : ℝ≥0∞ :=
⨅ (μ : OuterMeasure α) (_ : μ ∈ m), μ s