Prod

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

Statistics

Metric	Count
Definitions	0
Theorems prod, prod, subset_tangentConeAt_prod_left, subset_tangentConeAt_prod_right	4
Total	4

UniqueDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod 📖	mathematical	UniqueDiffOn	Prod.instAddCommGroup Prod.instModule AddCommGroup.toAddCommMonoid instTopologicalSpaceProd SProd.sprod Set Set.instSProd	—	UniqueDiffWithinAt.prod

UniqueDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod 📖	mathematical	UniqueDiffWithinAt	Prod.instAddCommGroup Prod.instModule AddCommGroup.toAddCommMonoid instTopologicalSpaceProd SProd.sprod Set Set.instSProd	—	uniqueDiffWithinAt_iff closure_prod_eq Submodule.span_mono Set.union_subset subset_tangentConeAt_prod_left subset_tangentConeAt_prod_right Dense.mono SetLike.le_def instIsConcreteLE LinearMap.span_inl_union_inr Dense.prod

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
subset_tangentConeAt_prod_left 📖	mathematical	Set Set.instMembership closure	Set.instHasSubset Set.image DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Prod.instAddCommMonoid Prod.instModule LinearMap.instFunLike LinearMap.inl 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 Prod.instAddCommGroup Prod.instSMul instTopologicalSpaceProd SProd.sprod Set.instSProd	—	tangentConeAt_closure Prod.continuousAdd Prod.continuousConstSMul closure_prod_eq exists_fun_of_mem_tangentConeAt mem_tangentConeAt_of_seq Filter.Tendsto.prodMk_nhds tendsto_const_nhds Filter.Eventually.mono add_zero subset_closure smul_zero
subset_tangentConeAt_prod_right 📖	mathematical	Set Set.instMembership closure	Set.instHasSubset Set.image DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Prod.instAddCommMonoid Prod.instModule LinearMap.instFunLike LinearMap.inr 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 Prod.instAddCommGroup Prod.instSMul instTopologicalSpaceProd SProd.sprod Set.instSProd	—	tangentConeAt_closure Prod.continuousAdd Prod.continuousConstSMul closure_prod_eq exists_fun_of_mem_tangentConeAt mem_tangentConeAt_of_seq Filter.Tendsto.prodMk_nhds tendsto_const_nhds Filter.Eventually.mono add_zero subset_closure smul_zero

---

← Back to Index