update — Mathlib

English

For DecidableEq ι, the map (f,i) ↦ update f i g is continuous in (f,g) for fixed i.

Русский

При конечном множестве индексов ι отображение (f,i) ↦ update f i g непрерывно по паре (f,g) для фиксированного i.

LaTeX

$$$\text{Continuous}(f) \Rightarrow \forall i,\, \text{Continuous}ig( (f,g) \mapsto \operatorname{update}(f(i),i,g)\big)$$$

Lean4

theorem update [DecidableEq ι] (hf : Continuous f) (i : ι) {g : X → A i} (hg : Continuous g) :
    Continuous fun a => update (f a) i (g a) :=
  continuous_iff_continuousAt.2 fun _ => hf.continuousAt.update i hg.continuousAt

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