Theorem Function.FactorsThrough.norm_extend'

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.norm_extend'View on Github →