piMap — Mathlib

English

If each coordinate function f_i is ContinuousAt at x_i, then Pi.map f is ContinuousAt at x.

Русский

Если каждая координатная функция f_i непрерывна в x_i, то Pi.map f непрерывно в x.

LaTeX

$$$$ \mathrm{ContinuousAt}(\Pi.map f, x) $$$$

Lean4

@[fun_prop]
protected theorem piMap {f : ∀ i, A i → B i} {x : ∀ i, A i} (hf : ∀ i, ContinuousAt (f i) (x i)) :
    ContinuousAt (Pi.map f) x :=
  continuousAt_pi.2 fun i ↦ (hf i).comp (continuousAt_apply i x)

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