Commit 2024-12-12 18:27 3c9302f1

View on Github →

feat(FaaDiBruno): add norm_compAlongOrderedFinpartitionL_le (#19713)

Estimated changes

Modified Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean

modified theorem OrderedFinpartition.compAlongOrderFinpartition_apply

modified def OrderedFinpartition.compAlongOrderedFinpartition

modified theorem OrderedFinpartition.compAlongOrderedFinpartitionL_apply

added theorem OrderedFinpartition.norm_applyOrderedFinpartition_le

added theorem OrderedFinpartition.norm_compAlongOrderedFinpartitionL_le

added theorem OrderedFinpartition.norm_compAlongOrderedFinpartition_le