equicontinuous_iff_range — Mathlib

English

A family F is equicontinuous iff the range family is equicontinuous.

Русский

Семейство функций эконтинуировано тогда и только тогда, когда эконтинуированно множество функций из диапазона.

LaTeX

$$$\\operatorname{Equicontinuous} F \\iff \\operatorname{Equicontinuous} \\bigl((\\uparrow) : \\operatorname{range} F \\to X \\to \\alpha\\bigr).$$$

Lean4

/-- A family `𝓕 : ι → X → α` is equicontinuous iff `range 𝓕` is equicontinuous,
i.e the family `(↑) : range F → X → α` is equicontinuous. -/
theorem equicontinuous_iff_range {F : ι → X → α} : Equicontinuous F ↔ Equicontinuous ((↑) : range F → X → α) :=
  forall_congr' fun _ => equicontinuousAt_iff_range

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