Commit 2024-02-05 20:21 328b7ecb

View on Github →

chore(fun_prop): move examples to a separate test file (#10281) chore(fun_prop): move examples to a separate test file

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Tactic.lean

Renamed Mathlib/Tactic/FunProp/AEMesurable.lean to Mathlib/Tactic/FunProp/AEMeasurable.lean

Modified Mathlib/Tactic/FunProp/ContDiff.lean

Modified Mathlib/Tactic/FunProp/Continuous.lean

Modified Mathlib/Tactic/FunProp/Differentiable.lean

Modified Mathlib/Tactic/FunProp/Measurable.lean

deleted theorem ContinuousOn.log'

Modified scripts/noshake.json

Created test/fun_prop2.lean

added theorem ContinuousOn.log'

added def foo