update — Mathlib

English

Let i be an index. If f: X → ∀ i, A_i is continuous at x, and g: X → A_i is continuous at x, then a ↦ update (f a) i (g a) is continuous at x.

Русский

Пусть i — индекс. Если f: X → ∀ i, A_i непрерывно в x и g: X → A_i непрерывно в x, то x ↦ update (f x) i (g x) непрерывно в x.

LaTeX

$$$\text{ContinuousAt}(f, x) \land \text{ContinuousAt}(g, x) \Rightarrow \text{ContinuousAt}\big( a \mapsto \operatorname{update}(f(a),i,g(a))\big)\, x$$$

Lean4

theorem update [DecidableEq ι] {x : X} (hf : ContinuousAt f x) (i : ι) {g : X → A i} (hg : ContinuousAt g x) :
    ContinuousAt (fun a => update (f a) i (g a)) x :=
  hf.tendsto.update i hg

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