Theorem Function.FactorsThrough.nnnorm_extend_one

Modification history

2026-10-02 14:34
Mathlib/Analysis/Normed/Group/Constructions.lean
feat(Analysis/Normed): sup norm of Function.extend by one (#44378)
Added Function.FactorsThrough.nnnorm_extend_oneView on Github →