matrix — Mathlib

English

If S is an open subset of R, then the set of matrices whose entries lie in S is open in M_{m,n}(R).

Русский

Если S — открытое подмножество R, то множество матриц с элементами из S открыто в M_{m,n}(R).

LaTeX

$$$\text{IsOpen}(S) \Rightarrow \text{IsOpen}(S.\mathrm{matrix})$$$

Lean4

theorem matrix [Finite m] [Finite n] [TopologicalSpace R] {S : Set R} (hS : IsOpen S) :
    IsOpen (S.matrix : Set (Matrix m n R)) :=
  Set.matrix_eq_pi ▸
    (isOpen_set_pi Set.finite_univ fun _ _ => isOpen_set_pi Set.finite_univ fun _ _ => hS).preimage continuous_id

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