Pi

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

Statistics

Metric	Count
Definitions	0
Theorems pi, univ_pi, pi, univ_pi, mapsTo_tangentConeAt_pi	5
Total	5

UniqueDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pi 📖	mathematical	ContinuousAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid ContinuousSMul 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 UniqueDiffOn	Pi.addCommGroup Pi.module Pi.topologicalSpace Set.pi	—	UniqueDiffWithinAt.pi
univ_pi 📖	mathematical	ContinuousAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid ContinuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction UniqueDiffOn	Pi.addCommGroup Pi.module Pi.topologicalSpace Set.pi Set.univ	—	UniqueDiffWithinAt.univ_pi Set.mem_univ

UniqueDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pi 📖	mathematical	ContinuousAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid ContinuousSMul 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 UniqueDiffWithinAt	Pi.addCommGroup Pi.module Pi.topologicalSpace Set.pi	—	Set.univ_pi_piecewise_univ univ_pi ContinuousSMul.continuousConstSMul Set.piecewise_eq_of_mem Set.piecewise_eq_of_notMem
univ_pi 📖	mathematical	ContinuousAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid ContinuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction UniqueDiffWithinAt	Pi.addCommGroup Pi.module Pi.topologicalSpace Set.pi Set.univ	—	closure_pi_set Dense.of_closure Dense.mono RingHomSurjective.ids Submodule.map_span closure_mono instIsConcreteLE iSup_le Submodule.span_mono Set.MapsTo.image_subset mapsTo_tangentConeAt_pi Dense.closure dense_pi

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapsTo_tangentConeAt_pi 📖	mathematical	ContinuousAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid ContinuousConstSMul 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	Set.MapsTo Pi.single NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid tangentConeAt Pi.addCommGroup Pi.instSMul Pi.topologicalSpace Set.pi Set.univ	—	tangentConeAt_closure Pi.continuousAdd instContinuousConstSMulForall exists_fun_of_mem_tangentConeAt mem_tangentConeAt_of_seq tendsto_pi_nhds eq_or_ne Pi.single_eq_same Pi.single_eq_of_ne Filter.Eventually.mono closure_pi_set Set.mem_univ_pi subset_closure add_zero smul_zero

---

← Back to Index