CauSeqFilter

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

Statistics

Metric	Count
Definitions	0
Theorems cauchySeq, tendsto_limit, isCauSeq, completeSpace_of_cauSeq_isComplete, isCauSeq_iff_cauchySeq	5
Total	5

CauSeq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cauchySeq 📖	mathematical	—	CauchySeq PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Nat.instPreorder IsCauSeq Real Real.instField Real.linearOrder Real.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing Norm.norm NormedField.toNorm	—	Real.instIsStrictOrderedRing cauchy_iff Filter.map_neBot Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Metric.mem_uniformity_dist cauchy₂ NormMulClass.isAbsoluteValue_norm NormedDivisionRing.toNormMulClass dist_eq_norm
tendsto_limit 📖	mathematical	—	Filter.Tendsto IsCauSeq Real Real.instField Real.linearOrder Real.instIsStrictOrderedRing NormedRing.toRing Norm.norm NormedRing.toNorm Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing lim	—	Real.instIsStrictOrderedRing tendsto_nhds Metric.isOpen_iff equiv_lim dist_comm dist_eq_norm instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat

CauchySeq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCauSeq 📖	mathematical	CauchySeq PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Nat.instPreorder	IsCauSeq Real Real.instField Real.linearOrder Real.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing Norm.norm NormedField.toNorm	—	Real.instIsStrictOrderedRing cauchy_iff Metric.dist_mem_uniformity instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat dist_eq_norm Set.mk_mem_prod le_refl

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
completeSpace_of_cauSeq_isComplete 📖	mathematical	—	CompleteSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	—	Real.instIsStrictOrderedRing NormMulClass.isAbsoluteValue_norm NormedDivisionRing.toNormMulClass Metric.complete_of_cauchySeq_tendsto isCauSeq_iff_cauchySeq Metric.tendsto_atTop CauSeq.equiv_lim dist_eq_norm
isCauSeq_iff_cauchySeq 📖	mathematical	—	IsCauSeq Real Real.instField Real.linearOrder Real.instIsStrictOrderedRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing Norm.norm NormedField.toNorm CauchySeq PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Nat.instPreorder	—	Real.instIsStrictOrderedRing CauSeq.cauchySeq CauchySeq.isCauSeq

---

← Back to Index