Continuous.matrix_elem
theorem Continuous.matrix_elem :
∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace X]
[inst_1 : TopologicalSpace R] {A : X → Matrix m n R},
Continuous A → ∀ (i : m) (j : n), Continuous fun x => A x i j
The theorem `Continuous.matrix_elem` states that given any topological space `X`, types `m`, `n`, a type `R` with a topological structure, and a continuous function `A` mapping from `X` to a matrix of type `Matrix m n R`, for each element (i,j) in the matrix, the function that maps an element `x` in `X` to the (i,j)-th element of the matrix `A(x)` is also continuous.
More concisely: Given a continuous function `A : X -> Matrix m n R` from a topological space `X` to a matrix of type `Matrix m n R`, the (i,j)-th entry function `x => A x!{i,j}` is continuous.
|
Continuous.matrix_det
theorem Continuous.matrix_det :
∀ {X : Type u_1} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace R]
[inst_2 : Fintype n] [inst_3 : DecidableEq n] [inst_4 : CommRing R] [inst_5 : TopologicalRing R]
{A : X → Matrix n n R}, Continuous A → Continuous fun x => (A x).det
The theorem `Continuous.matrix_det` states that for any type `X` with a topological space structure, type `n` with a finite number of elements and decidable equality, and ring `R` with a commutative ring structure and a topological ring structure, if `A` is a continuous function from `X` to the matrices of dimension `n x n` over `R`, then the function which assigns to each `x` in `X` the determinant of the matrix `A(x)` is also continuous. In other words, the determinant operation preserves continuity when applied on continuous functions from a topological space to the set of matrices over a topological ring.
More concisely: The determinant function of matrices is continuous when mapped from a continuous function of a topological space to the set of matrices over a topological ring.
|
Continuous.matrix_transpose
theorem Continuous.matrix_transpose :
∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace X]
[inst_1 : TopologicalSpace R] {A : X → Matrix m n R}, Continuous A → Continuous fun x => (A x).transpose
The theorem `Continuous.matrix_transpose` states that for any types `X`, `m`, `n`, and `R` where `X` is a topological space and `R` is a topological space, if `A` is a function from `X` to matrices of type `Matrix m n R` and `A` is continuous, then the function that applies `Matrix.transpose` to `A x` for each `x` in `X` is also continuous. In other words, if we have a continuous function that generates a matrix for each point in a topological space, then the function that generates the transpose of these matrices is also continuous.
More concisely: If `A : X -> Matrix m n R` is a continuous function from a topological space `X` to matrices of type `Matrix m n R`, then the function `x => Matrix.transpose (A x)` is also continuous.
|
continuousAt_matrix_inv
theorem continuousAt_matrix_inv :
∀ {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace R] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
[inst_3 : CommRing R] [inst_4 : TopologicalRing R] (A : Matrix n n R),
ContinuousAt Ring.inverse A.det → ContinuousAt Inv.inv A
The theorem `continuousAt_matrix_inv` states that for a type `n` and a type `R` with a topology (i.e., `R` is a topological space), where `R` is a commutative ring and a topological ring, and `n` is a finite type with decidable equality, if the `Ring.inverse` function is continuous at the determinant of a square matrix `A` with entries in `R` and dimensions indexed by `n`, then the matrix inverse function `Inv.inv` is also continuous at `A`. In simpler terms, if the function that calculates the inverse of the determinant of a matrix is continuous at a certain point, then the function that calculates the matrix inverse is also continuous at that same point. This theorem is particularly applicable in the context of normed rings or topological fields.
More concisely: If the determinant function is continuous at a matrix `A` and `R` is a topological ring with a commutative ring structure and decidable equality, then the matrix inverse function is continuous at `A`.
|
continuous_matrix
theorem continuous_matrix :
∀ {α : Type u_2} {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace R]
[inst_1 : TopologicalSpace α] {f : α → Matrix m n R},
(∀ (i : m) (j : n), Continuous fun a => f a i j) → Continuous f
This theorem states that for a function `f` mapping from a type `α` to a matrix with entries in `R`, rows indexed by `m` and columns indexed by `n`, if every coefficient of the resulting matrix is a continuous function of `α`, then the entire function `f` is also continuous. Here, `R` is equipped with a topological space structure, as is `α`. In other words, to establish the continuity of a function into matrices, it is sufficient to demonstrate that the coefficients of the matrix output by the function are all continuous functions.
More concisely: If every entry of a continuous function from a topological space to the space of matrices over a topological ring is continuous, then the function is continuous.
|
Continuous.matrix_mul
theorem Continuous.matrix_mul :
∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [inst : TopologicalSpace X]
[inst_1 : TopologicalSpace R] [inst_2 : Fintype n] [inst_3 : Mul R] [inst_4 : AddCommMonoid R]
[inst_5 : ContinuousAdd R] [inst_6 : ContinuousMul R] {A : X → Matrix m n R} {B : X → Matrix n p R},
Continuous A → Continuous B → Continuous fun x => A x * B x
This theorem states that for square matrices, if `A` and `B` are continuous functions from a topological space `X` to the space of matrices over a ring `R` (where `R` has a topological structure and `R`'s addition and multiplication operations are continuous), then the function that maps each `x` in `X` to the product of the matrices `A(x)` and `B(x)` is also continuous. Here, `m`, `n`, and `p` are types used to index the rows and columns of the matrices, and `n` is assumed to be a finite type, meaning that each matrix has only finitely many entries.
More concisely: Given square matrices `A` and `B` as continuous functions from a topological space `X` to the ring `R` with finite index types `m` and `n`, the function `x => A x * B x` is continuous from `X` to the space of `m x m` matrices over `R`.
|
Continuous.matrix_conjTranspose
theorem Continuous.matrix_conjTranspose :
∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace X]
[inst_1 : TopologicalSpace R] [inst_2 : Star R] [inst_3 : ContinuousStar R] {A : X → Matrix m n R},
Continuous A → Continuous fun x => (A x).conjTranspose
The theorem `Continuous.matrix_conjTranspose` states that for any types `X`, `m`, `n`, and `R` where `X` is endowed with a topological space structure, `R` is endowed with both a topological space structure and a star operation that is continuous, and `A` is a continuous function from `X` to matrices of type `m` by `n` with entries in `R`, the function that sends each element `x` in `X` to the conjugate transpose of the matrix `A(x)` is also continuous.
More concisely: If `X` is a topological space, `R` is a topological space with a continuous star operation, and `A` is a continuous function from `X` to matrices of size `m` by `n` over `R`, then the function sending `x` to the conjugate transpose of `A(x)` is continuous.
|