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