comp — Mathlib

English

Taking subfamilies preserves equicontinuity at a point. If F is equicontinuous at x0 and u: κ → ι, then F ∘ u is equicontinuous at x0.

Русский

Пусть F экконтинуально в точке x0, и есть отображение u: κ → ι; тогда F ∘ u эквонтинуально в x0.

LaTeX

$$$\\text{EquicontinuousAt}(F, x_0) \\Rightarrow \\forall u : κ \\to ι,\\ EquicontinuousAt (F \\circ u) x_0$$$

Lean4

/-- Taking sub-families preserves equicontinuity at a point. -/
theorem comp {F : ι → X → α} {x₀ : X} (h : EquicontinuousAt F x₀) (u : κ → ι) : EquicontinuousAt (F ∘ u) x₀ :=
  fun U hU => (h U hU).mono fun _ H k => H (u k)

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