Theorem tangentConeAt_of_mem_nhds

Modification history

2026-01-25 09:47
Mathlib/Analysis/Calculus/TangentCone/Basic.lean
refactor(TangentCone): redefine for TVS (#34127) …
Modified tangentConeAt_of_mem_nhdsView on Github →
2025-11-24 23:37
Mathlib/Analysis/Calculus/TangentCone/Basic.lean
feat(Analysis): Poincaré lemma for 1-forms (#24019)
Added tangentConeAt_of_mem_nhdsView on Github →