Cauchy

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

Statistics

Metric	Count
Definitions	0
Theorems cauchySeq_iff, cauchySeq_iff', complete_of_cauchySeq_tendsto, complete_of_convergent_controlled_sequences, exists_subseq_bounded_of_cauchySeq, uniformCauchySeqOn_iff, cauchySeq_bdd, cauchySeq_iff_le_tendsto_0, cauchySeq_of_le_tendsto_0, cauchySeq_of_le_tendsto_0'	10
Total	10

Metric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cauchySeq_iff 📖	mathematical	—	CauchySeq PseudoMetricSpace.toUniformSpace PartialOrder.toPreorder SemilatticeSup.toPartialOrder Real Real.instLT Dist.dist PseudoMetricSpace.toDist	—	Filter.HasBasis.cauchySeq_iff uniformity_basis_dist
cauchySeq_iff' 📖	mathematical	—	CauchySeq PseudoMetricSpace.toUniformSpace PartialOrder.toPreorder SemilatticeSup.toPartialOrder Real Real.instLT Dist.dist PseudoMetricSpace.toDist	—	Filter.HasBasis.cauchySeq_iff' uniformity_basis_dist
complete_of_cauchySeq_tendsto 📖	mathematical	Filter.Tendsto Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	CompleteSpace	—	EMetric.complete_of_cauchySeq_tendsto
complete_of_convergent_controlled_sequences 📖	mathematical	Real Real.instLT Real.instZero Filter.Tendsto Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	CompleteSpace	—	UniformSpace.complete_of_convergent_controlled_sequences EMetric.instIsCountablyGeneratedUniformity dist_mem_uniformity
exists_subseq_bounded_of_cauchySeq 📖	mathematical	CauchySeq PseudoMetricSpace.toUniformSpace Nat.instPreorder Real Real.instLT Real.instZero	StrictMono Dist.dist PseudoMetricSpace.toDist	—	Filter.eventually_atTop instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat cauchySeq_iff LE.le.trans Filter.extraction_forall_of_eventually
uniformCauchySeqOn_iff 📖	mathematical	—	UniformCauchySeqOn PseudoMetricSpace.toUniformSpace Filter.atTop PartialOrder.toPreorder SemilatticeSup.toPartialOrder Real Real.instLT Dist.dist PseudoMetricSpace.toDist	—	mem_uniformity_dist Filter.eventually_atTop_prod_self' SemilatticeSup.instIsDirectedOrder Filter.Eventually.mono Filter.prod_atTop_atTop_eq Filter.eventually_atTop LE.le.ge

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cauchySeq_bdd 📖	mathematical	CauchySeq PseudoMetricSpace.toUniformSpace Nat.instPreorder	Real Real.instLT Real.instZero Dist.dist PseudoMetricSpace.toDist	—	Metric.cauchySeq_iff' zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing add_pos_of_nonneg_of_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid le_or_gt lt_of_lt_of_le le_add_of_nonneg_left covariant_swap_add_of_covariant_add Finset.le_sup Finset.mem_range lt_of_le_of_lt lt_add_of_pos_right add_pos dist_triangle_right add_lt_add IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd
cauchySeq_iff_le_tendsto_0 📖	mathematical	—	CauchySeq PseudoMetricSpace.toUniformSpace Nat.instPreorder Real Real.instLE Real.instZero Dist.dist PseudoMetricSpace.toDist Filter.Tendsto Filter.atTop nhds UniformSpace.toTopologicalSpace Real.pseudoMetricSpace	—	cauchySeq_bdd le_of_lt le_csSup le_rfl dist_self Metric.tendsto_atTop Nat.instAtLeastTwoHAddOfNat Real.dist_0_eq_abs abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid lt_of_le_of_lt csSup_le le_trans half_lt_self PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Metric.cauchySeq_iff half_pos cauchySeq_of_le_tendsto_0
cauchySeq_of_le_tendsto_0 📖	mathematical	Real Real.instLE Dist.dist PseudoMetricSpace.toDist Filter.Tendsto Filter.atTop PartialOrder.toPreorder SemilatticeSup.toPartialOrder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	CauchySeq	—	cauchySeq_of_le_tendsto_0' le_rfl
cauchySeq_of_le_tendsto_0' 📖	mathematical	Real Real.instLE Dist.dist PseudoMetricSpace.toDist Filter.Tendsto Filter.atTop PartialOrder.toPreorder SemilatticeSup.toPartialOrder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	CauchySeq	—	Metric.cauchySeq_iff' dist_comm Filter.Eventually.exists Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder Filter.Tendsto.eventually gt_mem_nhds instOrderTopologyReal

---

← Back to Index