matrix_replicateRow — Mathlib

English

If A: X → n → R is continuous, then the matrix obtained by replicating A across a index set ι (replicateRow ι (A x)) is continuous as a function of x.

Русский

Если A: X → n → R непрерывна, то матрица, полученная повторением A по индексу ι (replicateRow ι (A x)), непрерывна по x.

LaTeX

$$$\\operatorname{Continuous}\\big(\\lambda x:\\,X,\\ \\mathrm{replicateRow}\\ ι\\ (A\\,x)\\big).$$$

Lean4

@[continuity, fun_prop]
theorem matrix_replicateRow {ι : Type*} {A : X → n → R} (hA : Continuous A) :
    Continuous fun x => replicateRow ι (A x) :=
  continuous_matrix fun _ _ => (continuous_apply _).comp hA

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