Theorems · Definition · measure theory

MeasureTheory.extend

{α : Type u_2} → {P : α → Prop} → ((s : α) → P s → ENNReal) → α → ENNReal

We can trivially extend a function defined on a subclass of objects (with codomain ℝ≥0∞) to all objects by defining it to be ∞ on the objects not in the class.

Defined in

Mathlib.MeasureTheory.OuterMeasure.Induced

Cited by

24 results in Mathlib

Foundations

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