Mathlib Map

Theorems · Theorem · general topology

cauchy_pure

∀ {α : Type u} [uniformSpace : UniformSpace α] {a : α}, Cauchy (pure a)
Defined in
Mathlib.Topology.UniformSpace.Cauchy
Cited by
2 results in Mathlib
Foundations
Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
UniformSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CauchyFilter.pureCauchy · cited by 9CauchyFilter.pureCauchyCompleteSpace.fst_of_prod · cited by 2CompleteSpace.fst_of_prodCompleteSpace.snd_of_prod · cited by 1CompleteSpace.snd_of_prodFilter · cited by 8121FilterUniformSpace · cited by 2040UniformSpaceCauchy · cited by 115Cauchypure_le_nhds · cited by 39pure_le_nhdscauchy_nhds · cited by 7cauchy_nhdsCauchy.mono · cited by 6Cauchy.monocauchy_pureCITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by3

Results whose statement or proof uses this declaration.