Commit 2026-10-02 14:34 6620c780

View on Github →

feat(Analysis/Normed): sup norm of Function.extend by one (#44378)

Estimated changes

Modified Mathlib/Analysis/Normed/Group/Constructions.lean

added theorem Function.FactorsThrough.nnnorm_extend'

added theorem Function.FactorsThrough.nnnorm_extend_one

added theorem Function.FactorsThrough.norm_extend'

added theorem Function.FactorsThrough.norm_extend_one

added theorem Pi.nnnorm_extend_le'

added theorem Pi.norm_extend_le'

added theorem pi_nnnorm_comp_le'

modified theorem pi_norm_comp_le'

Modified Mathlib/Data/Set/Restrict.lean

modified theorem Set.range_extend

modified theorem Set.range_extend_subset

Modified Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean

added theorem ciSup_extend

added theorem ciSup_extend_le