Theorem posTangentConeAt_univ

Modification history

2026-01-25 09:47
Mathlib/Analysis/Calculus/LocalExtr/Basic.lean
refactor(TangentCone): redefine for TVS (#34127) …
Modified posTangentConeAt_univView on Github →
2023-05-29 19:05
Mathlib/Analysis/Calculus/LocalExtr.lean
feat: port Analysis.Calculus.LocalExtr (#4247)
Added posTangentConeAt_univView on Github →