Theorems · Theorem · general topology

CauchySeq.mem_entourage

∀ {α : Type u} [uniformSpace : UniformSpace α] {β : Type u_1} [inst : SemilatticeSup β] {u : β → α},
  CauchySeq u → ∀ {V : SetRel α α}, V ∈ uniformity α → ∃ k₀, ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V

Defined in

Mathlib.Topology.UniformSpace.Cauchy

Cited by

1 results in Mathlib

Foundations

Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

UniformSpaceSemilatticeSup