uniformContinuous_dom₂ — Mathlib

English

For a function f on SeparationQuotient α × SeparationQuotient β, uniform continuity of f is equivalent to uniform continuity of its lift to α × β via mk.

Русский

Для функции f на SeparationQuotient α × SeparationQuotient β равномерная непрерывность f эквивалентна равномерной непрерывности её подъёма на α × β через mk.

LaTeX

$$$UniformContinuous\ f \iff UniformContinuous\ (\lambda p: (\mk p.1, \mk p.2))$$$

Lean4

theorem uniformContinuous_dom₂ {f : SeparationQuotient α × SeparationQuotient β → γ} :
    UniformContinuous f ↔ UniformContinuous fun p : α × β ↦ f (mk p.1, mk p.2) :=
  by
  simp only [UniformContinuous, uniformity_prod_eq_prod, uniformity_eq, prod_map_map_eq, tendsto_map'_iff]
  rfl

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