Commit 2024-07-13 21:21 548ca520

View on Github →

feat(LocalExtr/Basic): add lemmas about _ ∈ posTangentConeAt _ _ (#14434)

Estimated changes

Modified Mathlib/Analysis/Calculus/Darboux.lean

Modified Mathlib/Analysis/Calculus/LocalExtr/Basic.lean

modified theorem IsLocalMaxOn.fderivWithin_eq_zero

modified theorem IsLocalMaxOn.fderivWithin_nonpos

modified theorem IsLocalMaxOn.hasFDerivWithinAt_eq_zero

modified theorem IsLocalMaxOn.hasFDerivWithinAt_nonpos

modified theorem IsLocalMinOn.fderivWithin_eq_zero

modified theorem IsLocalMinOn.fderivWithin_nonneg

modified theorem IsLocalMinOn.hasFDerivWithinAt_eq_zero

modified theorem IsLocalMinOn.hasFDerivWithinAt_nonneg

added theorem mem_posTangentConeAt_of_frequently_mem

deleted theorem mem_posTangentConeAt_of_segment_subset'

modified theorem mem_posTangentConeAt_of_segment_subset

added theorem one_mem_posTangentConeAt_iff_frequently

added theorem one_mem_posTangentConeAt_iff_mem_closure

added theorem sub_mem_posTangentConeAt_of_segment_subset