mono — Mathlib

English

Let F be uniformly equicontinuous on T and S ⊆ T; then F is uniformly equicontinuous on S.

Русский

Пусть F равномерно эконтинуально на T и S ⊆ T; тогда F равномерно эконтинуально на S.

LaTeX

$$$$ \operatorname{UniformEquicontinuousOn} F T \land S\subseteq T \Rightarrow \operatorname{UniformEquicontinuousOn} F S. $$$$

Lean4

theorem mono {F : ι → β → α} {S T : Set β} (H : UniformEquicontinuousOn F T) (hST : S ⊆ T) :
    UniformEquicontinuousOn F S := fun U hU ↦ (H U hU).filter_mono <| by gcongr

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