equicontinuousOn_iff_range — Mathlib

English

A family F is EquicontinuousOn F S iff the range family is EquicontinuousOn ((↑) : range F → X → α) S.

Русский

Эконтинуированность на S эквивалентна эконтинуированности диапазона на S.

LaTeX

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

Lean4

/-- A family `𝓕 : ι → X → α` is equicontinuous on `S` iff `range 𝓕` is equicontinuous on `S`,
i.e the family `(↑) : range F → X → α` is equicontinuous on `S`. -/
theorem equicontinuousOn_iff_range {F : ι → X → α} {S : Set X} :
    EquicontinuousOn F S ↔ EquicontinuousOn ((↑) : range F → X → α) S :=
  forall_congr' fun _ ↦ forall_congr' fun _ ↦ equicontinuousWithinAt_iff_range

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