continuous_precomp' — Mathlib

English

For any φ: ι' → ι, the precomposition map f ↦ f ∘ φ is continuous on function spaces.

Русский

Для любого φ: ι' → ι отображение f ↦ f ∘ φ непрерывно на пространствах функций.

LaTeX

$$$$ \mathrm{Continuous}(\,\lambda f. f \circ \phi\, ) $$$$

Lean4

theorem continuous_precomp' {ι' : Type*} (φ : ι' → ι) : Continuous (fun (f : (∀ i, A i)) (j : ι') ↦ f (φ j)) :=
  continuous_pi fun j ↦ continuous_apply (φ j)

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