Commit 2025-04-28 13:10 8a1d355d

View on Github →

chore(TangentCone): fix names (#24426) Use tangentConeAt, not tangentCone in lemma names.

Estimated changes

Modified Mathlib/Analysis/Calculus/TangentCone.lean

added theorem mapsTo_tangentConeAt_pi

deleted theorem mapsTo_tangentCone_pi

added theorem mem_tangentConeAt_of_openSegment_subset

added theorem mem_tangentConeAt_of_segment_subset

deleted theorem mem_tangentCone_of_openSegment_subset

deleted theorem mem_tangentCone_of_segment_subset

added theorem subset_tangentConeAt_prod_left

added theorem subset_tangentConeAt_prod_right

deleted theorem subset_tangentCone_prod_left

deleted theorem subset_tangentCone_prod_right

added theorem tangentConeAt_congr

added theorem tangentConeAt_eq_univ

added theorem tangentConeAt_inter_nhds

added theorem tangentConeAt_mono

added theorem tangentConeAt_mono_nhds

added theorem tangentConeAt_nonempty_of_properSpace

added theorem tangentConeAt_univ

deleted theorem tangentCone_congr

deleted theorem tangentCone_eq_univ

deleted theorem tangentCone_inter_nhds

deleted theorem tangentCone_mono

deleted theorem tangentCone_mono_nhds

deleted theorem tangentCone_nonempty_of_properSpace

deleted theorem tangentCone_univ