ProdApproximation

📁 Source: Mathlib/Topology/UniformSpace/ProdApproximation.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_finite_sum_mul_approximation_of_mem_uniformity, exists_finite_sum_smul_approximation_of_mem_uniformity	2
Total	2

ContinuousMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_finite_sum_mul_approximation_of_mem_uniformity 📖	mathematical	Set Filter Filter.instMembership uniformity	Set.instMembership DFunLike.coe ContinuousMap instTopologicalSpaceProd UniformSpace.toTopologicalSpace instFunLike Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Finset.univ Fin.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	exists_finite_sum_smul_approximation_of_mem_uniformity
exists_finite_sum_smul_approximation_of_mem_uniformity 📖	mathematical	Set Filter Filter.instMembership uniformity	Set.instMembership DFunLike.coe ContinuousMap instTopologicalSpaceProd UniformSpace.toTopologicalSpace instFunLike Finset.sum AddCommGroup.toAddCommMonoid Finset.univ Fin.fintype SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SMulWithZero.toSMulZeroClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass MulActionWithZero.toSMulWithZero	—	mem_compactConvergence_entourage_iff isCompact_univ Set.instReflSubset IsTopologicalAddGroup.toContinuousAdd IsUniformAddGroup.to_topologicalAddGroup exists_finite_sum_const_indicator_approximation_of_mem_nhds_diagonal nhdsSet_diagonal_le_uniformity IsClopen.continuous_indicator TopologicalSpace.Clopens.isClopen continuous_const Finset.sum_congr sum_apply Set.indicator_of_mem one_smul Set.indicator_of_notMem zero_smul

---

← Back to Index