**measure space**if and only if

(1) | $(X, \mathcal{F})$ is a D1108: Measurable space |

(2) | $\mu$ is an D85: Unsigned basic measure on $(X, \mathcal{F})$ |

Definition D1158

Measure space

Formulation 0

A D5107: Triple $M = (X, \mathcal{F}, \mu)$ is a **measure space** if and only if

(1) | $(X, \mathcal{F})$ is a D1108: Measurable space |

(2) | $\mu$ is an D85: Unsigned basic measure on $(X, \mathcal{F})$ |

Subdefinitions

▶ | D1159: Probability space |

Children

▶ | D4248: Almost everywhere constant map |

▶ | D2940: Measure-preserving endomorphism |

▶ | D1159: Probability space |

▶ | D1732: Pushforward measure |

Results