Commit 2024-09-03 09:13 ce66aa03

View on Github →

feat(Order/Lattice): add Monotone.of_map_inf_le_left etc (#15508)

Add Monotone.of_map_inf_le_left etc.
Use Monotone.of_left_le_map_sup to reorganize the proof of SimpleFunc.lintegral_mono.
Add gcongr attrs.

Estimated changes

Modified Mathlib/MeasureTheory/Function/SimpleFunc.lean

added theorem MeasureTheory.SimpleFunc.lintegral_mono_fun

added theorem MeasureTheory.SimpleFunc.lintegral_mono_measure

added theorem MeasureTheory.SimpleFunc.map_fst_pair

added theorem MeasureTheory.SimpleFunc.map_snd_pair

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

Modified Mathlib/Order/Lattice.lean

added theorem Monotone.of_le_map_sup

added theorem Monotone.of_left_le_map_sup

added theorem Monotone.of_map_inf_le

added theorem Monotone.of_map_inf_le_left