uniformContinuous_precomp — Mathlib

English

Let α_i be spaces with UniformSpace structures, and φ: ι' → ι. The map f ↦ f ∘ φ from ∏_{i∈ι} α_i to ∏_{j∈ι'} α_{φ(j)} is uniformly continuous (in particular, continuous).

Русский

Пусть для каждого i ∈ ι задано пространство α_i с униформной структурой, и пусть φ: ι' → ι. Отображение f ↦ f ∘ φ из ∏_{i∈ι} α_i в ∏_{j∈ι'} α_{φ(j)} равномерно непрерывно (а значит и непрерывно).

LaTeX

$$$UniformContinuous\\big( f \\mapsto f \\circ \\varphi \\big)$$$

Lean4

theorem uniformContinuous_precomp (φ : ι' → ι) : UniformContinuous (· ∘ φ : (ι → β) → (ι' → β)) :=
  Pi.uniformContinuous_precomp' _ φ

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