comp — Mathlib

English

Taking sub-families preserves equicontinuity on a subset: if h : EquicontinuousOn F S, then for any u, EquicontinuousOn (F ∘ u) S.

Русский

Если F эконтинуально на S, то F ∘ u эконтинуально на S для любого отображения u.

LaTeX

$$EquicontinuousOn F S → ∀ u: κ → ι, EquicontinuousOn (F ∘ u) S$$

Lean4

/-- Taking sub-families preserves equicontinuity on a subset. -/
theorem comp {F : ι → X → α} {S : Set X} (h : EquicontinuousOn F S) (u : κ → ι) : EquicontinuousOn (F ∘ u) S :=
  fun x hx ↦ (h x hx).comp u

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