comp — Mathlib

English

Taking subfamilies preserves equicontinuity at a point within a subset. If h: EquicontinuousWithinAt F S x0, then F ∘ u is EquicontinuousWithinAt S x0 for any u: κ → ι.

Русский

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

LaTeX

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

Lean4

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

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