Commit 2025-04-23 09:07 435a8219

View on Github →

feat(TangentCone): add tangentConeAt_closure (#24272) Also add gcongr to tangentCone_mono.

Estimated changes

Modified Mathlib/Analysis/Calculus/TangentCone.lean

added theorem UniqueDiffWithinAt.mono_closure

added theorem tangentConeAt_closure

added theorem uniqueDiffWithinAt_closure