Theorems · Inductive type · measure theory

MeasureTheory.Measure

(α : Type u_6) → [MeasurableSpace α] → Type u_6

A measure is defined to be an outer measure that is countably additive on measurable sets, with the additional assumption that the outer measure is the canonical extension of the restricted measure. The measure of a set s, denoted μ s, is an extended nonnegative real. The real-valued version is written μ.real s.

Defined in

Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Cited by

10,939 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

MeasurableSpace