Theorems · Definition · measure theory

MeasureTheory.OuterMeasure.sInfGen

{α : Type u_1} → Set (MeasureTheory.OuterMeasure α) → Set α → ENNReal

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.

Defined in

Mathlib.MeasureTheory.OuterMeasure.OfFunction

Cited by

4 results in Mathlib

Foundations

Depth 126 from the axioms · uses propext, Classical.choice, Quot.sound