matrix_replicateCol — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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