comp — Mathlib

English

Taking sub-indexes preserves equicontinuity: if F is equicontinuous, then for every u : κ → ι, F ∘ u is equicontinuous.

Русский

Сохранение эконтинуальности при предкомпозиции: если F эконтинуальна, то для любого отображения u : κ → ι имеем F ∘ u эконтинуальность.

LaTeX

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

Lean4

/-- Taking sub-families preserves equicontinuity. -/
theorem comp {F : ι → X → α} (h : Equicontinuous F) (u : κ → ι) : Equicontinuous (F ∘ u) := fun x => (h x).comp u

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