Theorems · Theorem · general topology

tendsto_diag_uniformity

∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] (f : β → α) (l : Filter β),
  Filter.Tendsto (fun x => (f x, f x)) l (uniformity α)

Relation fun f g ↦ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α) is reflexive.

Defined in

Mathlib.Topology.UniformSpace.Defs

Cited by

2 results in Mathlib

Foundations

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

Assumes

UniformSpace