mono — Mathlib

English

If F is equicontinuous on a set T, then it is equicontinuous on every subset S ⊆ T.

Русский

Если F равномерно непрерывно на множестве T, то оно равномерно непрерывно на любом подмножестве S ⊆ T.

LaTeX

$$$$ \operatorname{EquicontinuousOn} F T \ \\text{and } S\subseteq T \Longrightarrow \operatorname{EquicontinuousOn} F S. $$$$

Lean4

theorem mono {F : ι → X → α} {S T : Set X} (H : EquicontinuousOn F T) (hST : S ⊆ T) : EquicontinuousOn F S := fun x hx ↦
  (H x (hST hx)).mono hST

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