uniformEquicontinuousOn — Mathlib

English

If F is uniformly equicontinuous, then its restriction to any set S is uniformly equicontinuous on S.

Русский

Если F равномерно эконтинуально, то его ограничение на любое множество S также равномерно эконтинуально на S.

LaTeX

$$$$ \operatorname{UniformEquicontinuous} F \Rightarrow \operatorname{UniformEquicontinuousOn} F S. $$$$

Lean4

theorem uniformEquicontinuousOn {F : ι → β → α} (H : UniformEquicontinuous F) (S : Set β) :
    UniformEquicontinuousOn F S := fun U hU ↦ (H U hU).filter_mono inf_le_left

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