Commit 2023-05-15 10:06 618546f7

View on Github →

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

Estimated changes

added theorem IsOpen.uniqueDiffOn
added theorem UniqueDiffOn.inter
added theorem UniqueDiffOn.pi
added theorem UniqueDiffOn.prod
added theorem UniqueDiffOn.univ_pi
added def UniqueDiffOn
added theorem UniqueDiffWithinAt.pi
added structure UniqueDiffWithinAt
added theorem mapsTo_tangentCone_pi
added theorem tangentConeAt.lim_zero
added def tangentConeAt
added theorem tangentCone_congr
added theorem tangentCone_inter_nhds
added theorem tangentCone_mono
added theorem tangentCone_mono_nhds
added theorem tangentCone_univ
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 uniqueDiffOn_empty
added theorem uniqueDiffOn_univ
added theorem uniqueDiffWithinAt_Iio
added theorem uniqueDiffWithinAt_Ioi
added theorem uniqueDiffWithinAt_Ioo