tendsto_diag_uniformity — Mathlib

English

For any function f: β → α, Tendsto (x ↦ (f x, f x)) l (𝓤 α).

Русский

Для любой функции f: β → α выполняется Tendsto (x, f(x), f(x)) к 𝓤 α.

LaTeX

$$$$\\forall f: \\beta \\to \\alpha,\\;\\mathrm{Tendsto}(x \\mapsto (f x, f x))\\ l\\ (𝓤 α).$$$$

Lean4

/-- Relation `fun f g ↦ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α)` is reflexive. -/
theorem tendsto_diag_uniformity (f : β → α) (l : Filter β) : Tendsto (fun x => (f x, f x)) l (𝓤 α) := fun _s hs =>
  mem_map.2 <| univ_mem' fun _ => refl_mem_uniformity hs

Похожие утверждения