Equicontinuity

📁 Source: Mathlib/Topology/MetricSpace/Equicontinuity.lean

Statistics

Metric	Count
Definitions	0
Theorems equicontinuousAt_iff, equicontinuousAt_iff_pair, equicontinuousAt_iff_right, equicontinuousAt_of_continuity_modulus, equicontinuous_of_continuity_modulus, uniformEquicontinuous_iff, uniformEquicontinuous_iff_right, uniformEquicontinuous_of_continuity_modulus	8
Total	8

Metric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equicontinuousAt_iff 📖	mathematical	—	EquicontinuousAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real Real.instLT Real.instZero Dist.dist PseudoMetricSpace.toDist	—	Filter.HasBasis.equicontinuousAt_iff nhds_basis_ball uniformity_basis_dist
equicontinuousAt_iff_pair 📖	mathematical	—	EquicontinuousAt PseudoMetricSpace.toUniformSpace Set Filter Filter.instMembership nhds Real Real.instLT Dist.dist PseudoMetricSpace.toDist	—	equicontinuousAt_iff_pair dist_mem_uniformity mem_uniformity_dist
equicontinuousAt_iff_right 📖	mathematical	—	EquicontinuousAt PseudoMetricSpace.toUniformSpace Filter.Eventually nhds	—	Filter.HasBasis.equicontinuousAt_iff_right uniformity_basis_dist
equicontinuousAt_of_continuity_modulus 📖	mathematical	Filter.Tendsto Real nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Filter.Eventually	EquicontinuousAt	—	equicontinuousAt_iff_right Filter.mp_mem Iio_mem_nhds instClosedIciTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal Filter.univ_mem' LE.le.trans_lt
equicontinuous_of_continuity_modulus 📖	mathematical	Filter.Tendsto Real nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Real.instLE Dist.dist PseudoMetricSpace.toDist	Equicontinuous	—	UniformEquicontinuous.equicontinuous uniformEquicontinuous_of_continuity_modulus
uniformEquicontinuous_iff 📖	mathematical	—	UniformEquicontinuous PseudoMetricSpace.toUniformSpace Real Real.instLT Real.instZero Dist.dist PseudoMetricSpace.toDist	—	Filter.HasBasis.uniformEquicontinuous_iff uniformity_basis_dist
uniformEquicontinuous_iff_right 📖	mathematical	—	UniformEquicontinuous PseudoMetricSpace.toUniformSpace Filter.Eventually uniformity	—	Filter.HasBasis.uniformEquicontinuous_iff_right uniformity_basis_dist
uniformEquicontinuous_of_continuity_modulus 📖	mathematical	Filter.Tendsto Real nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Real.instLE Dist.dist PseudoMetricSpace.toDist	UniformEquicontinuous	—	uniformEquicontinuous_iff tendsto_nhds_nhds le_abs_self sub_zero tsub_zero AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid abs_dist

---

← Back to Index