Commit 2025-11-06 17:28 7e5b7078

View on Github →

chore(TangentCone): split file (#30932) It will be easier for me to generalize the definition this way.

Estimated changes

deleted theorem Convex.span_tangentConeAt
deleted theorem IsOpen.uniqueDiffOn
deleted theorem IsOpen.uniqueDiffWithinAt
deleted theorem UniqueDiffOn.inter
deleted theorem UniqueDiffOn.mono_field
deleted theorem UniqueDiffOn.pi
deleted theorem UniqueDiffOn.prod
deleted theorem UniqueDiffOn.univ_pi
deleted def UniqueDiffOn
deleted theorem UniqueDiffWithinAt.accPt
deleted theorem UniqueDiffWithinAt.inter'
deleted theorem UniqueDiffWithinAt.inter
deleted theorem UniqueDiffWithinAt.mono
deleted theorem UniqueDiffWithinAt.pi
deleted theorem UniqueDiffWithinAt.prod
deleted structure UniqueDiffWithinAt
deleted theorem mapsTo_tangentConeAt_pi
deleted theorem tangentConeAt.lim_zero
deleted def tangentConeAt
deleted theorem tangentConeAt_closure
deleted theorem tangentConeAt_congr
deleted theorem tangentConeAt_eq_univ
deleted theorem tangentConeAt_inter_nhds
deleted theorem tangentConeAt_mono
deleted theorem tangentConeAt_mono_field
deleted theorem tangentConeAt_mono_nhds
deleted theorem tangentConeAt_subset_zero
deleted theorem tangentConeAt_univ
deleted theorem uniqueDiffOn_Icc
deleted theorem uniqueDiffOn_Icc_zero_one
deleted theorem uniqueDiffOn_Ici
deleted theorem uniqueDiffOn_Ico
deleted theorem uniqueDiffOn_Iic
deleted theorem uniqueDiffOn_Iio
deleted theorem uniqueDiffOn_Ioc
deleted theorem uniqueDiffOn_Ioi
deleted theorem uniqueDiffOn_Ioo
deleted theorem uniqueDiffOn_convex
deleted theorem uniqueDiffOn_empty
deleted theorem uniqueDiffOn_univ
deleted theorem uniqueDiffWithinAt_Ici
deleted theorem uniqueDiffWithinAt_Iic
deleted theorem uniqueDiffWithinAt_Iio
deleted theorem uniqueDiffWithinAt_Ioi
deleted theorem uniqueDiffWithinAt_Ioo
deleted theorem uniqueDiffWithinAt_congr
deleted theorem uniqueDiffWithinAt_convex
deleted theorem uniqueDiffWithinAt_inter'
deleted theorem uniqueDiffWithinAt_inter
deleted theorem uniqueDiffWithinAt_univ
deleted theorem zero_mem_tangentCone
added theorem IsOpen.uniqueDiffOn
added theorem UniqueDiffOn.inter
added theorem tangentConeAt.lim_zero
added theorem tangentConeAt_closure
added theorem tangentConeAt_congr
added theorem tangentConeAt_mono
added theorem tangentConeAt_univ
added theorem uniqueDiffOn_empty
added theorem uniqueDiffOn_univ
added theorem zero_mem_tangentCone
added def UniqueDiffOn
added structure UniqueDiffWithinAt
added def tangentConeAt
added theorem tangentConeAt_eq_univ
added theorem UniqueDiffOn.pi
added theorem UniqueDiffOn.univ_pi
added theorem UniqueDiffWithinAt.pi
added theorem UniqueDiffOn.prod
added theorem uniqueDiffOn_Icc
added theorem uniqueDiffOn_Ici
added theorem uniqueDiffOn_Ico
added theorem uniqueDiffOn_Iic
added theorem uniqueDiffOn_Iio
added theorem uniqueDiffOn_Ioc
added theorem uniqueDiffOn_Ioi
added theorem uniqueDiffOn_Ioo
added theorem uniqueDiffOn_convex
added theorem uniqueDiffWithinAt_Ici
added theorem uniqueDiffWithinAt_Iic
added theorem uniqueDiffWithinAt_Iio
added theorem uniqueDiffWithinAt_Ioi
added theorem uniqueDiffWithinAt_Ioo