uniformContinuous — Mathlib

English

Each function in a uniformly equicontinuous family is uniformly continuous.

Русский

Каждая функция из равномерно равноконтинуального семейства является равномерно непрерывной.

LaTeX

$$$\\forall i : ι,\\ UniformContinuous (F_i)$$$

Lean4

/-- Each function of a uniformly equicontinuous family is uniformly continuous. -/
theorem uniformContinuous {F : ι → β → α} (h : UniformEquicontinuous F) (i : ι) : UniformContinuous (F i) := fun U hU =>
  mem_map.mpr (mem_of_superset (h U hU) fun _ hxy => hxy i)

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