continuous_pi — Mathlib

English

If each coordinate map i ↦ f i is continuous, then the combined map f is continuous.

Русский

Если каждая координатная карта i ↦ f_i непрерывна, то совокупное отображение f непрерывно.

LaTeX

$$$$ \forall i, \operatorname{Continuous}(\lambda a. f(a)_i) \Rightarrow \operatorname{Continuous}(f) $$$$

Lean4

@[continuity, fun_prop]
theorem continuous_pi (h : ∀ i, Continuous fun a => f a i) : Continuous f :=
  continuous_pi_iff.2 h

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