Basic

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

Statistics

Metric	Count
Definitions	0
Theorems `of_mem_tangentConeAt_ne_zero`, `tangentConeAt_eq_biInter_closure`, `uniqueDiffOn`, `uniqueDiffWithinAt`, `inter`, `mono_field`, `accPt`, `closure`, `congr_pt`, `inter`, `inter'`, `mono`, `mono_closure`, `mono_field`, `mono_nhds`, `of_closure`, `mem_closure_of_nonempty_tangentConeAt`, `mem_tangentConeAt_of_add_smul_mem`, `tangentConeAt_closure`, `tangentConeAt_congr`, `tangentConeAt_eq_biInter_closure`, `tangentConeAt_inter_nhds`, `tangentConeAt_mono`, `tangentConeAt_mono_field`, `tangentConeAt_mono_nhds`, `tangentConeAt_of_mem_nhds`, `tangentConeAt_subset_zero`, `tangentConeAt_univ`, `uniqueDiffOn_empty`, `uniqueDiffOn_univ`, `uniqueDiffWithinAt_closure`, `uniqueDiffWithinAt_congr`, `uniqueDiffWithinAt_inter`, `uniqueDiffWithinAt_inter'`, `uniqueDiffWithinAt_of_mem_nhds`, `uniqueDiffWithinAt_univ`, `zero_mem_tangentCone`, `zero_mem_tangentConeAt`, `zero_mem_tangentConeAt_iff`	39
Total	39

AccPt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_mem_tangentConeAt_ne_zero` 📖	mathematical	`Set` `Set.instMembership` `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` `AddCommGroup.toAddCommMonoid`	`AccPt` `Filter.principal`	—	`Mathlib.Tactic.Contrapose.contrapose₂` `tangentConeAt_subset_zero`

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tangentConeAt_eq_biInter_closure` 📖	mathematical	`Filter.HasBasis` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`tangentConeAt` `Set.iInter` `closure` `Set` `Set.smul` `Set.univ` `Set.instInter` `Set.preimage` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`Set.ext` `tangentConeAt_def` `clusterPt_iff_forall_mem_closure` `map` `top_prod` `nhdsWithin_hasBasis` `Set.image_prod`

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`uniqueDiffOn` 📖	mathematical	`IsOpen`	`UniqueDiffOn` `DivisionSemiring.toSemiring`	—	`uniqueDiffWithinAt`
`uniqueDiffWithinAt` 📖	mathematical	`IsOpen` `Set` `Set.instMembership`	`UniqueDiffWithinAt` `DivisionSemiring.toSemiring`	—	`uniqueDiffWithinAt_of_mem_nhds` `mem_nhds`

UniqueDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inter` 📖	mathematical	`UniqueDiffOn` `IsOpen`	`Set` `Set.instInter`	—	`UniqueDiffWithinAt.inter` `IsOpen.mem_nhds`
`mono_field` 📖	—	`UniqueDiffOn`	—	—	`UniqueDiffWithinAt.mono_field`

UniqueDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`accPt` 📖	mathematical	`UniqueDiffWithinAt`	`AccPt` `Filter.principal`	—	`Dense.mono` `instIsConcreteLE` `Submodule.span_mono` `tangentConeAt_subset_zero` `dense_tangentConeAt` `Submodule.span_zero` `IsClosed.closure_eq` `T2Space.t1Space`
`closure` 📖	mathematical	`UniqueDiffWithinAt`	`closure`	—	`mono` `subset_closure`
`congr_pt` 📖	—	`UniqueDiffWithinAt`	—	—	—
`inter` 📖	mathematical	`UniqueDiffWithinAt` `Set` `Filter` `Filter.instMembership` `nhds`	`Set.instInter`	—	`uniqueDiffWithinAt_inter`
`inter'` 📖	mathematical	`UniqueDiffWithinAt` `Set` `Filter` `Filter.instMembership` `nhdsWithin`	`Set.instInter`	—	`uniqueDiffWithinAt_inter'`
`mono` 📖	—	`UniqueDiffWithinAt` `Set` `Set.instHasSubset`	—	—	`uniqueDiffWithinAt_iff` `Dense.mono` `instIsConcreteLE` `Submodule.span_mono` `tangentConeAt_mono` `Set.mem_of_subset_of_mem` `closure_mono`
`mono_closure` 📖	—	`UniqueDiffWithinAt` `Set` `Set.instHasSubset` `closure`	—	—	`of_closure` `mono`
`mono_field` 📖	—	`UniqueDiffWithinAt`	—	—	`Dense.mono` `instIsConcreteLE` `Submodule.span_mono` `tangentConeAt_mono_field`
`mono_nhds` 📖	—	`UniqueDiffWithinAt` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhdsWithin`	—	—	`mem_closure_iff_nhdsWithin_neBot` `Dense.mono` `Submodule.span_mono` `tangentConeAt_mono_nhds` `Filter.NeBot.mono`
`of_closure` 📖	—	`UniqueDiffWithinAt` `closure`	—	—	`uniqueDiffWithinAt_closure`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_closure_of_nonempty_tangentConeAt` 📖	mathematical	`Set.Nonempty` `tangentConeAt`	`Set` `Set.instMembership` `closure`	—	`exists_fun_of_mem_tangentConeAt` `mem_closure_of_tendsto` `add_zero` `Filter.Tendsto.add` `tendsto_const_nhds`
`mem_tangentConeAt_of_add_smul_mem` 📖	mathematical	`Filter.Tendsto` `nhdsWithin` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Filter.Eventually` `Set.instMembership` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`tangentConeAt`	—	`mem_tangentConeAt_of_seq` `zero_smul` `Filter.Tendsto.smul` `tendsto_nhdsWithin_iff` `tendsto_const_nhds` `tendsto_nhds_of_eventually_eq` `Filter.Eventually.mono` `inv_smul_smul₀`
`tangentConeAt_closure` 📖	mathematical	—	`tangentConeAt` `closure`	—	`Set.Subset.antisymm` `Filter.HasBasis.tangentConeAt_eq_biInter_closure` `nhds_basis_opens` `Set.iInter₂_mono` `closure_minimal` `Mathlib.Tactic.GCongr.rel_imp_rel` `Set.instIsTransSubset` `Set.smul_subset_smul` `subset_refl` `Set.instReflSubset` `Set.inter_subset_inter` `IsOpenMap.preimage_closure_subset_closure_preimage` `isOpenMap_add_left` `IsOpen.inter_closure` `set_smul_closure_subset` `isClosed_closure` `tangentConeAt_mono` `subset_closure`
`tangentConeAt_congr` 📖	mathematical	`nhdsWithin`	`tangentConeAt`	—	`Set.Subset.antisymm` `tangentConeAt_mono_nhds` `Eq.le` `Eq.ge`
`tangentConeAt_eq_biInter_closure` 📖	mathematical	—	`tangentConeAt` `Set.iInter` `Set` `Filter` `Filter.instMembership` `nhds` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `closure` `Set.smul` `Set.univ` `Set.instInter` `Set.preimage` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`Filter.HasBasis.tangentConeAt_eq_biInter_closure` `Filter.basis_sets`
`tangentConeAt_inter_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`tangentConeAt` `Set.instInter`	—	`tangentConeAt_congr` `nhdsWithin_restrict'`
`tangentConeAt_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`tangentConeAt`	—	`tangentConeAt_def` `ClusterPt.mono` `Filter.smul_le_smul` `le_refl` `nhdsWithin_mono` `Set.preimage_mono`
`tangentConeAt_mono_field` 📖	mathematical	—	`Set` `Set.instHasSubset` `tangentConeAt` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`tangentConeAt_def` `ClusterPt.mono` `smul_one_smul` `Filter.isScalarTower''` `le_imp_le_of_le_of_le` `Filter.smul_le_smul` `le_top` `le_refl`
`tangentConeAt_mono_nhds` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhdsWithin`	`Set` `Set.instHasSubset` `tangentConeAt`	—	`tangentConeAt_def` `ClusterPt.mono` `Filter.smul_le_smul` `le_refl` `nhdsWithin_le_iff` `Filter.Tendsto.inf` `Continuous.tendsto'` `continuous_add_left` `add_zero` `Set.MapsTo.tendsto` `Set.mapsTo_preimage` `tendsto_nhdsWithin_iff` `Filter.Tendsto.mono_right`
`tangentConeAt_of_mem_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`tangentConeAt` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Set.univ`	—	`Set.univ_inter` `tangentConeAt_inter_nhds` `tangentConeAt_univ`
`tangentConeAt_subset_zero` 📖	mathematical	`AccPt` `Filter.principal`	`Set` `Set.instHasSubset` `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` `AddCommGroup.toAddCommMonoid` `Set.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`exists_fun_of_mem_tangentConeAt` `add_zero` `Filter.Tendsto.add` `tendsto_const_nhds` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Filter.Eventually.mp` `Filter.Tendsto.eventually` `Filter.Eventually.mono` `smul_zero` `tendsto_nhds_unique_of_eventuallyEq`
`tangentConeAt_univ` 📖	mathematical	—	`tangentConeAt` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `Set.univ`	—	`tangentConeAt_def` `nhdsWithin_univ` `Filter.top_smul_nhds_zero`
`uniqueDiffOn_empty` 📖	mathematical	—	`UniqueDiffOn` `Set` `Set.instEmptyCollection`	—	—
`uniqueDiffOn_univ` 📖	mathematical	—	`UniqueDiffOn` `DivisionSemiring.toSemiring` `Set.univ`	—	`uniqueDiffWithinAt_univ`
`uniqueDiffWithinAt_closure` 📖	mathematical	—	`UniqueDiffWithinAt` `closure`	—	`tangentConeAt_closure` `IsClosed.closure_eq`
`uniqueDiffWithinAt_congr` 📖	mathematical	`nhdsWithin`	`UniqueDiffWithinAt`	—	`UniqueDiffWithinAt.mono_nhds` `le_of_eq`
`uniqueDiffWithinAt_inter` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`UniqueDiffWithinAt` `Set.instInter`	—	`uniqueDiffWithinAt_congr` `nhdsWithin_restrict'`
`uniqueDiffWithinAt_inter'` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsWithin`	`UniqueDiffWithinAt` `Set.instInter`	—	`uniqueDiffWithinAt_congr` `nhdsWithin_restrict''`
`uniqueDiffWithinAt_of_mem_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`UniqueDiffWithinAt` `DivisionSemiring.toSemiring`	—	`Set.univ_inter` `UniqueDiffWithinAt.inter` `uniqueDiffWithinAt_univ`
`uniqueDiffWithinAt_univ` 📖	mathematical	—	`UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Set.univ`	—	`uniqueDiffWithinAt_iff` `tangentConeAt_univ` `Submodule.span_univ` `IsClosed.closure_eq`
`zero_mem_tangentCone` 📖	mathematical	`Set` `Set.instMembership` `closure`	`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` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`zero_mem_tangentConeAt`
`zero_mem_tangentConeAt` 📖	mathematical	`Set` `Set.instMembership` `closure`	`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` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`mem_tangentConeAt_of_frequently` `Continuous.tendsto'` `Continuous.fun_add` `continuous_id'` `continuous_const` `add_neg_cancel` `add_neg_cancel_comm_assoc` `mem_closure_iff_frequently` `one_smul`
`zero_mem_tangentConeAt_iff` 📖	mathematical	—	`Set` `Set.instMembership` `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` `AddCommGroup.toAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `closure`	—	`mem_closure_of_nonempty_tangentConeAt` `zero_mem_tangentConeAt`

---

← Back to Index