Theorem MeasureTheory.Measure.le_intro

Modification history

2026-08-20 12:42

Mathlib/MeasureTheory/Measure/CompleteLattice.lean

chore: split too long file Measure.MeasureSpace (#42949) …

Modified MeasureTheory.Measure.le_intro View on Github →

2024-02-21 16:46

Mathlib/MeasureTheory/Measure/MeasureSpace.lean

refactor(MeasureTheory): redefine `≤` on measures (#10714) …

Added MeasureTheory.Measure.le_intro View on Github →