matrix_map — Mathlib

English

If A: X → M_{m×n}(S) is continuous and f: S → R is continuous, then the matrix map A(x).map f is continuous as a function of x.

Русский

Если A: X → M_{m×n}(S) непрерывна, и f: S → R непрерывно, то отображение x ↦ (A(x)).map f непрерывно по x.

LaTeX

$$$\\operatorname{Continuous}\\big( x \\mapsto (A(x)).\\operatorname{map} f \\big).$$$

Lean4

@[continuity, fun_prop]
theorem matrix_map [TopologicalSpace S] {A : X → Matrix m n S} {f : S → R} (hA : Continuous A) (hf : Continuous f) :
    Continuous fun x => (A x).map f :=
  continuous_matrix fun _ _ => hf.comp <| hA.matrix_elem _ _

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