Theorem ciSup_extend_le

Modification history

2026-10-02 14:34
Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
feat(Analysis/Normed): sup norm of Function.extend by one (#44378)
Added ciSup_extend_leView on Github →