Theorems · Definition · measure theory

MeasureTheory.inducedOuterMeasure

{α : Type u_1} →
  {P : Set α → Prop} → (m : (s : Set α) → P s → ENNReal) → (P0 : P ∅) → m ∅ P0 = 0 → MeasureTheory.OuterMeasure α

Given an arbitrary function on a subset of sets, we can define the outer measure corresponding to it (this is the unique maximal outer measure that is at most m on the domain of m).

Defined in

Mathlib.MeasureTheory.OuterMeasure.Induced

Cited by

22 results in Mathlib

Foundations

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