Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-05-15 10:06
618546f7
View on Github →
feat: port Analysis.Calculus.TangentCone (
#3636
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Analysis/Calculus/TangentCone.lean
added
theorem
IsOpen.uniqueDiffOn
added
theorem
IsOpen.uniqueDiffWithinAt
added
theorem
UniqueDiffOn.inter
added
theorem
UniqueDiffOn.pi
added
theorem
UniqueDiffOn.prod
added
theorem
UniqueDiffOn.uniqueDiffWithinAt
added
theorem
UniqueDiffOn.univ_pi
added
def
UniqueDiffOn
added
theorem
UniqueDiffWithinAt.inter'
added
theorem
UniqueDiffWithinAt.inter
added
theorem
UniqueDiffWithinAt.mono
added
theorem
UniqueDiffWithinAt.mono_nhds
added
theorem
UniqueDiffWithinAt.pi
added
theorem
UniqueDiffWithinAt.prod
added
theorem
UniqueDiffWithinAt.univ_pi
added
structure
UniqueDiffWithinAt
added
theorem
mapsTo_tangentCone_pi
added
theorem
mem_tangentCone_of_openSegment_subset
added
theorem
mem_tangentCone_of_segment_subset
added
theorem
subset_tangentCone_prod_left
added
theorem
subset_tangentCone_prod_right
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_Icc_zero_one
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
added
theorem
uniqueDiffWithinAt_congr
added
theorem
uniqueDiffWithinAt_convex
added
theorem
uniqueDiffWithinAt_inter'
added
theorem
uniqueDiffWithinAt_inter
added
theorem
uniqueDiffWithinAt_of_mem_nhds
added
theorem
uniqueDiffWithinAt_univ