Theorem MonotoneOn.csInf_eq_of_subset_of_forall_exists_le

Modification history

2025-02-14 10:09
Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
feat: left and right derivatives of a convex function (#21063) …
Added MonotoneOn.csInf_eq_of_subset_of_forall_exists_leView on Github →