English
Let i be a fixed column index. If A: X → M_{m×n}(R) and B: X → R^m are continuous, then the map x ↦ (A(x)) with its i-th column replaced by B(x) is continuous.
Русский
Пусть i — фиксированный индекс столбца. Если A: X → M_{m×n}(R) и B: X → R^m непрерывны, то отображение x ↦ (A(x)) с замененной i-й колонкой на B(x) непрерывно.
LaTeX
$$$\\operatorname{Continuous}(A) \\land \\operatorname{Continuous}(B) \\Rightarrow \\operatorname{Continuous}\\bigl(x \\mapsto (A(x)).\\mathrm{updateCol}\\,i\\,(B(x))\\bigr)$$$
Lean4
@[continuity, fun_prop]
theorem matrix_updateCol [DecidableEq n] (i : n) {A : X → Matrix m n R} {B : X → m → R} (hA : Continuous A)
(hB : Continuous B) : Continuous fun x => (A x).updateCol i (B x) :=
continuous_matrix fun _j k =>
(continuous_apply k).comp <| ((continuous_apply _).comp hA).update i ((continuous_apply _).comp hB)
