uniformContinuousOn — Mathlib

English

Each function of a uniformly equicontinuous family on S is uniformly continuous on S.

Русский

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

LaTeX

$$$\\forall i : ι,\\ F_i \\text{ UniformContinuousOn } S$$$

Lean4

/-- Each function of a family uniformly equicontinuous on `S` is uniformly continuous on `S`. -/
theorem uniformContinuousOn {F : ι → β → α} {S : Set β} (h : UniformEquicontinuousOn F S) (i : ι) :
    UniformContinuousOn (F i) S := fun U hU => mem_map.mpr (mem_of_superset (h U hU) fun _ hxy => hxy i)

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