Theorem MeasureTheory.SimpleFunc.map_fst_pair

Modification history

2024-09-03 09:13
Mathlib/MeasureTheory/Function/SimpleFunc.lean
feat(Order/Lattice): add Monotone.of_map_inf_le_left etc (#15508) …
Added MeasureTheory.SimpleFunc.map_fst_pairView on Github →