Theorem MonotoneOn.csSup_eq_of_subset_of_forall_exists_le

Modification history

2026-08-10 08:17
Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
chore(order/ConditionallyCompleteLattice): use `to_dual` more (#41558) …
Deleted MonotoneOn.csSup_eq_of_subset_of_forall_exists_leView on Github →
2025-02-14 10:09
Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
feat: left and right derivatives of a convex function (#21063) …
Added MonotoneOn.csSup_eq_of_subset_of_forall_exists_leView on Github →