Commit 2026-04-17 18:09 dbbf3f76

View on Github →

feat(Analysis/Calculus/ContDiff): add notation ℕ∞ω for WithTop ℕ∞ (#34649) Add a ContDiff-scoped notation ℕ∞ω for WithTop ℕ∞, accompanying the existing notations ∞ and ω for (⊤ : ℕ∞) : ℕ∞ω and ⊤ : ℕ∞ω.

Estimated changes

modified theorem contDiff_prodAssoc
modified theorem contDiff_prodAssoc_symm
modified theorem norm_iteratedFDeriv_comp_le
modified theorem norm_iteratedFDeriv_mul_le
modified theorem norm_iteratedFDeriv_smul_le
modified theorem CPolynomialAt.contDiffAt
modified theorem CPolynomialOn.contDiffOn
modified def ContDiff
modified def ContDiffAt
modified def ContDiffOn
modified def ContDiffWithinAt
modified theorem HasFTaylorSeriesUpToOn.add
modified theorem contDiff_single
modified theorem contDiff_update
modified theorem hasFTaylorSeriesUpToOn_pi'
modified theorem hasFTaylorSeriesUpToOn_pi
modified theorem le_minSmoothness
modified theorem minSmoothness_add
modified theorem minSmoothness_eq_infty
modified structure IsContDiffImplicitAt
modified theorem Real.contDiffAt_log
modified theorem Real.contDiffOn_log
modified theorem Real.contDiffAt_arccos
modified theorem Real.contDiffAt_arccos_iff
modified theorem Real.contDiffAt_arcsin
modified theorem Real.contDiffAt_arcsin_iff
modified theorem Real.contDiffOn_arccos
modified theorem Real.contDiffOn_arcsin
modified theorem ContMDiff.extend_one
modified theorem contMDiffAt_subtype_iff
modified theorem contMDiff_inclusion
modified theorem contMDiff_subtype_val
modified def ContDiffWithinAtProp
modified def ContMDiff
modified def ContMDiffAt
modified def ContMDiffOn
modified def ContMDiffWithinAt
modified theorem contMDiffAt_iff
modified theorem contDiffOn_stereoToFun
modified theorem contDiff_stereoInvFunAux
modified theorem contMDiff_circleExp
modified theorem contMDiff_coe_sphere
modified theorem contMDiff_neg_sphere