mono — Mathlib

English

If H ⊆ X → α is equicontinuous at x0 on S and H' ⊆ H, then H' is equicontinuous at x0 on S.

Русский

Если семейство функций H ⊆ X → α эконтинуально в точке x0 на S, и H' ⊆ H, то H' тоже эконтинуально в x0 на S.

LaTeX

$$H.EquicontinuousWithinAt S x0 → H' ⊆ H → H'.EquicontinuousWithinAt S x0$$

Lean4

protected theorem mono {H H' : Set <| X → α} {S : Set X} {x₀ : X} (h : H.EquicontinuousWithinAt S x₀) (hH : H' ⊆ H) :
    H'.EquicontinuousWithinAt S x₀ :=
  h.comp (inclusion hH)

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