sInfGen — Mathlib

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

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