uniformContinuous_restrict — Mathlib

English

Let S ⊆ ι. The restriction map S.restrict: ∀ i, α_i → ∀ i ∈ S, α_i is uniformly continuous.

Русский

Пусть S ⊆ ι. Ограничение отображения S.restrict: (∀ i, α_i) → (∀ i ∈ S, α_i) равномерно непрерывно.

LaTeX

$$$UniformContinuous \\big( S.restrict \\big)$$$

Lean4

theorem uniformContinuous_restrict (S : Set ι) : UniformContinuous (S.restrict : (∀ i : ι, α i) → (∀ i : S, α i)) :=
  Pi.uniformContinuous_precomp' _ ((↑) : S → ι)

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