Commit 2023-05-30 10:47 9300e8ad

View on Github →

feat: port Analysis.Calculus.DiffContOnCl (#4492)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/DiffContOnCl.lean

added theorem DiffContOnCl.add

added theorem DiffContOnCl.add_const

added theorem DiffContOnCl.comp

added theorem DiffContOnCl.const_add

added theorem DiffContOnCl.const_smul

added theorem DiffContOnCl.const_sub

added theorem DiffContOnCl.continuousOn_ball

added theorem DiffContOnCl.differentiable_at'

added theorem DiffContOnCl.inv

added theorem DiffContOnCl.mk_ball

added theorem DiffContOnCl.neg

added theorem DiffContOnCl.smul

added theorem DiffContOnCl.smul_const

added theorem DiffContOnCl.sub

added theorem DiffContOnCl.sub_const

added structure DiffContOnCl

added theorem Differentiable.comp_diffContOnCl

added theorem Differentiable.diffContOnCl

added theorem DifferentiableOn.diffContOnCl

added theorem DifferentiableOn.diffContOnCl_ball

added theorem IsClosed.diffContOnCl_iff

added theorem diffContOnCl_const

added theorem diffContOnCl_univ