Theorem Function.extend_le_one

Modification history

2023-09-28 21:41
Mathlib/Algebra/Order/Pi.lean
feat: Extend a nonnegative function (#7418) …
Added Function.extend_le_oneView on Github →