Def tangentConeAt

Modification history

2026-01-25 09:47

Mathlib/Analysis/Calculus/TangentCone/Defs.lean

refactor(TangentCone): redefine for TVS (#34127) …

Deleted tangentConeAt View on Github →

2025-11-06 17:28

Mathlib/Analysis/Calculus/TangentCone.lean

chore(TangentCone): split file (#30932) …

Modified tangentConeAt View on Github →

2023-05-15 10:06

Mathlib/Analysis/Calculus/TangentCone.lean

feat: port Analysis.Calculus.TangentCone (#3636)

Added tangentConeAt View on Github →