uniformContinuous_def — Mathlib

English

Uniform continuity of a map f is equivalent to: for every entourage r in β, the preimage under (f×f) of r is an entourage in α.

Русский

Униформная непрерывность функции f эквивалентна: для каждого спутника r в β предобраз по (f×f) множества r является спутником в α.

LaTeX

$$$ UniformContinuous f \iff \forall r \in \mathcal{U}(\beta), \{(x,y) : (f x, f y) \in r\} \in \mathcal{U}(\alpha). $$$

Lean4

theorem uniformContinuous_def [UniformSpace β] {f : α → β} :
    UniformContinuous f ↔ ∀ r ∈ 𝓤 β, {x : α × α | (f x.1, f x.2) ∈ r} ∈ 𝓤 α :=
  Iff.rfl

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