Commit 2024-02-04 21:54 a619d25b

View on Github →

feat: fun_prop tactic for proving Continuous, Differentiable, Measurable, ... (#10040) New tactic fun_prop to prove FUNction PROPerties like continuity, differentiability, ...

Estimated changes

added def Lean.Expr.setArg
added theorem ContDiff.comp'
added theorem ContDiffAt.comp'
added theorem ContDiffOn.div'
added theorem contDiffAt_id'
added theorem contDiffAt_pi'
added theorem contDiffOn_id'
added theorem contDiffOn_pi'
added theorem contDiff_id'
added theorem contDiff_pi'
added theorem Continuous.div₀
added theorem ContinuousAt.comp'
added theorem ContinuousAt.div₀
added theorem ContinuousOn.comp''
added theorem ContinuousOn.div₀
added theorem continuousAt_id'
added theorem continuousAt_pi'
added theorem continuousOn_apply
added theorem continuousOn_id'
added theorem continuousOn_pi'
added theorem Differentiable.comp'
added theorem DifferentiableAt.comp'
added theorem DifferentiableOn.comp'
added theorem differentiableOn_id'
added theorem ContinuousOn.log'
added inductive StateList
added def StateListM
added def StateListT.run'
added def StateListT.run
added def StateListT
added structure ConHom
added theorem Con_apply
added theorem Con_applyDep
added theorem Con_comp
added theorem Con_const
added theorem Con_id
added theorem Con_pi
added structure LinHom
added theorem Lin_apply
added theorem Lin_applyDep
added theorem Lin_comp
added theorem Lin_id
added theorem Lin_pi
added theorem add_Con'
added theorem add_Con
added theorem conHom_con'
added theorem fst_Con'
added theorem fst_Con
added theorem linHom_lin
added theorem lin_to_con
added theorem prod_mk_Con
added theorem prod_mk_Lin
added theorem snd_Con'
added theorem snd_Con