comp — Mathlib

English

Let F: ι → β → α and S ⊆ β. If F is UniformEquicontinuousOn F S and u: κ → ι, then UniformEquicontinuousOn (F ∘ u) S.

Русский

Пусть F: ι → β → α и S ⊆ β. Если F является равномерно эконтинуированным на S, то подсемейство F ∘ u на S тоже таково.

LaTeX

$$$\\text{If }F: \\iota \\to \\beta \\to \\alpha\\text{ is UniformEquicontinuousOn }F\\,S\\text{ and }u: \\kappa \\to \\iota,\\; \\text{then } UniformEquicontinuousOn (F \\circ u) S.$$$

Lean4

/-- Taking sub-families preserves uniform equicontinuity on a subset. -/
theorem comp {F : ι → β → α} {S : Set β} (h : UniformEquicontinuousOn F S) (u : κ → ι) :
    UniformEquicontinuousOn (F ∘ u) S := fun U hU ↦ (h U hU).mono fun _ H k => H (u k)

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