d9_hasDerivWithinAt_sub_const
Provedd9_hasDerivWithinAt_sub_constcandidate-decomposition
Automatically extracted helper theorem d9_hasDerivWithinAt_sub_const from oversized parent candidate 029f41399a9b5b2cc3817d3867fba60227809162ca9c89b493c85daffb84e989.
Preamble
import Mathlib import Definitions.Def_NestedSeatAlloc_IntPolicy_Model open NestedSeatAlloc.IntPolicy
Formal statement
theorem d9_hasDerivWithinAt_sub_const
(g : ℝ → ℝ) (s x d : ℝ)
(hg : HasDerivWithinAt g d (Set.Ici (s - x)) (s - x)) :
HasDerivWithinAt (fun t => g (t - x)) d (Set.Ici s) s := by sorry
Source
candidate-decomposition:304a5ba4-c3fe-4878-9ae0-c209084c89c1:029f41399a9b5b2cc3817d3867fba60227809162ca9c89b493c85daffb84e989