Theorem Function.one_le_extend

Modification history

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