Documentation Verification Report

Defs

📁 Source: Mathlib/Analysis/Calculus/TangentCone/Defs.lean

Statistics

Metric	Count
Definitions `UniqueDiffOn`, `UniqueDiffWithinAt`, `posTangentConeAt`, `tangentConeAt`	4
Theorems `uniqueDiffWithinAt`, `dense_tangentConeAt`, `mem_closure`, `exists_fun_of_mem_tangentConeAt`, `mem_tangentConeAt_of_frequently`, `mem_tangentConeAt_of_seq`, `tangentConeAt_def`, `uniqueDiffWithinAt_iff`	8
Total	12

UniqueDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`uniqueDiffWithinAt` 📖	mathematical	`UniqueDiffOn` `Set` `Set.instMembership`	`UniqueDiffWithinAt`	—	—

UniqueDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dense_tangentConeAt` 📖	mathematical	`UniqueDiffWithinAt`	`Dense` `SetLike.coe` `Submodule` `AddCommGroup.toAddCommMonoid` `Submodule.setLike` `Submodule.span` `tangentConeAt` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	—
`mem_closure` 📖	mathematical	`UniqueDiffWithinAt`	`Set` `Set.instMembership` `closure`	—	—

(root)

Definitions

Name	Category	Theorems
`UniqueDiffOn` 📖	MathDef	26 math math: `uniqueDiffOn_Icc`, `uniqueDiffOn_Iic`, `UniqueMDiffOn.uniqueDiffOn`, `uniqueDiffOn_Ioc`, `ModelWithCorners.uniqueDiffOn_preimage`, `UniqueMDiffOn.uniqueDiffOn_target_inter`, `uniqueDiffOn_univ`, `uniqueDiffOn_convex`, `uniqueDiffOn_Icc_zero_one`, `Diffeomorph.uniqueDiffOn_image`, `UniqueMDiffOn.uniqueDiffOn_inter_preimage`, `uniqueDiffOn_Iio`, `uniqueMDiffOn_iff_uniqueDiffOn`, `Diffeomorph.uniqueDiffOn_preimage`, `uniqueDiffOn_Ioi`, `uniqueDiffOn_Ico`, `uniqueDiffOn_convex_of_isRCLikeNormedField`, `ContinuousLinearEquiv.uniqueDiffOn_preimage_iff`, `IsOpen.uniqueDiffOn`, `uniqueDiffOn_Ioo`, `ContinuousLinearEquiv.uniqueDiffOn_image_iff`, `ModelWithCorners.uniqueDiffOn_preimage_source`, `uniqueDiffOn_extChartAt_target`, `ModelWithCorners.uniqueDiffOn`, `uniqueDiffOn_Ici`, `uniqueDiffOn_empty`
`UniqueDiffWithinAt` 📖	CompData	26 math math: `uniqueDiffWithinAt_Iic`, `uniqueDiffWithinAt_closure`, `uniqueDiffWithinAt_of_mem_nhds`, `uniqueDiffWithinAt_iff_accPt`, `IsOpen.uniqueDiffWithinAt`, `UniqueDiffOn.uniqueDiffWithinAt`, `uniqueDiffWithinAt_convex_of_isRCLikeNormedField`, `uniqueDiffWithinAt_convex`, `uniqueDiffWithinAt_congr`, `uniqueDiffWithinAt_iff`, `UniqueDiffWithinAt.smul_iff`, `uniqueDiffWithinAt_Ioo`, `uniqueDiffWithinAt_Ioi`, `UniqueMDiffWithinAt.uniqueDiffWithinAt`, `uniqueDiffWithinAt_Iio`, `uniqueMDiffWithinAt_iff`, `uniqueMDiffWithinAt_iff_inter_range`, `AccPt.uniqueDiffWithinAt`, `uniqueDiffWithinAt_univ`, `ModelWithCorners.uniqueDiffWithinAt_image`, `uniqueDiffWithinAt_Ici`, `uniqueMDiffWithinAt_iff_uniqueDiffWithinAt`, `uniqueDiffWithinAt_extChartAt_target`, `UniqueMDiffOn.uniqueDiffWithinAt_range_inter`, `uniqueDiffWithinAt_inter`, `uniqueDiffWithinAt_inter'`
`posTangentConeAt` 📖	CompOp	7 math math: `one_mem_posTangentConeAt_iff_frequently`, `mem_posTangentConeAt_of_frequently_mem`, `mem_posTangentConeAt_of_segment_subset`, `one_mem_posTangentConeAt_iff_mem_closure`, `posTangentConeAt_mono`, `sub_mem_posTangentConeAt_of_segment_subset`, `posTangentConeAt_univ`
`tangentConeAt` 📖	CompOp	35 math math: `tangentConeAt_inter_nhds`, `tangentConeAt_nonempty_of_properSpace`, `tangentConeAt_eq_biInter_closure`, `tangentConeAt_univ`, `tangentConeAt_congr`, `mem_tangentConeAt_of_segment_subset`, `mem_tangentConeAt_of_pow_smul`, `tangentConeAt_mono`, `mem_tangentConeAt_of_frequently`, `UniqueDiffWithinAt.dense_tangentConeAt`, `Convex.span_tangentConeAt`, `subset_tangentConeAt_prod_right`, `subset_tangentConeAt_prod_left`, `uniqueDiffWithinAt_iff`, `tangentConeAt_of_mem_nhds`, `tangentConeAt_closure`, `HasFDerivWithinAt.mapsTo_tangent_cone`, `tangentConeAt_mono_nhds`, `tangentConeAt_def`, `tangentConeAt_real_subset_isRCLikeNormedField`, `tangentConeAt_mono_field`, `mem_tangentConeAt_iff_exists_seq`, `mapsTo_tangentConeAt_pi`, `HasFDerivWithinAt.unique_on`, `zero_mem_tangentConeAt`, `mem_tangentConeAt_of_openSegment_subset`, `mem_tangentConeAt_of_seq`, `sub_mem_posTangentConeAt_of_openSegment_subset`, `tangentConeAt_subset_zero`, `mem_tangentConeAt_iff_exists_seq_norm_tendsto_atTop`, `zero_mem_tangentConeAt_iff`, `mem_tangentConeAt_of_add_smul_mem`, `Filter.HasBasis.tangentConeAt_eq_biInter_closure`, `tangentConeAt_eq_univ`, `zero_mem_tangentCone`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_fun_of_mem_tangentConeAt` 📖	mathematical	`Set` `Set.instMembership` `tangentConeAt`	`Filter.Tendsto` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Filter.Eventually` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`Filter.neBot_inf_comap_iff_map'` `ClusterPt.eq_1` `Filter.map_prod_eq_map₂` `Filter.map₂_smul` `Set.mem_setOf` `tangentConeAt_def` `Filter.Tendsto.mono_left` `Filter.tendsto_snd` `LE.le.trans` `inf_le_right` `Filter.prod_mono` `le_refl` `nhdsWithin_le_nhds` `Filter.Eventually.filter_mono` `Filter.top_prod` `Filter.eventually_comap` `Filter.mp_mem` `eventually_mem_nhdsWithin` `Filter.univ_mem'` `Filter.tendsto_comap` `inf_le_left`
`mem_tangentConeAt_of_frequently` 📖	mathematical	`Filter.Tendsto` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Filter.Frequently` `Set` `Set.instMembership` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	`tangentConeAt`	—	`Filter.map₂_smul` `Filter.map_prod_eq_map₂` `Filter.Tendsto.comp` `Filter.tendsto_map` `Filter.Tendsto.prodMk` `Filter.tendsto_top` `tendsto_nhdsWithin_iff` `Filter.Tendsto.mono_left` `inf_le_left` `tangentConeAt_def` `ClusterPt.mono` `Filter.Tendsto.mapClusterPt` `Filter.frequently_iff_neBot`
`mem_tangentConeAt_of_seq` 📖	mathematical	`Filter.Tendsto` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Filter.Eventually` `Set` `Set.instMembership` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	`tangentConeAt`	—	`mem_tangentConeAt_of_frequently` `Filter.Eventually.frequently`
`tangentConeAt_def` 📖	mathematical	—	`tangentConeAt` `setOf` `ClusterPt` `Filter` `Filter.instSMul` `Top.top` `Filter.instTop` `nhdsWithin` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Set.preimage` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	—
`uniqueDiffWithinAt_iff` 📖	mathematical	—	`UniqueDiffWithinAt` `Dense` `SetLike.coe` `Submodule` `AddCommGroup.toAddCommMonoid` `Submodule.setLike` `Submodule.span` `tangentConeAt` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Set` `Set.instMembership` `closure`	—	—

---

← Back to Index