Matrix.IsAdjMatrix.adjMatrix_toGraph_eq
theorem Matrix.IsAdjMatrix.adjMatrix_toGraph_eq :
∀ {V : Type u_1} {α : Type u_2} [inst : MulZeroOneClass α] [inst_1 : Nontrivial α] {A : Matrix V V α}
(h : A.IsAdjMatrix) [inst_2 : DecidableEq α], SimpleGraph.adjMatrix α h.toGraph = A
This theorem states that if `A` is recognized as an adjacency matrix, then the adjacency matrix of the graph induced by `A` is `A` itself. In other words, if a matrix `A` satisfies the properties required for an adjacency matrix (as indicated by `A.IsAdjMatrix`), then the adjacency matrix produced by the graph that is derived from `A` (`h.toGraph`) will be equal to the original matrix `A`. The theorem applies to any types `V` and `α` that follow the conditions `MulZeroOneClass α`, `Nontrivial α`, and `DecidableEq α`, which refer to required properties of the elements in the matrix.
More concisely: If `A` is an adjacency matrix (i.e., satisfies the properties required for an adjacency matrix), then the adjacency matrix of the graph derived from `A` equals `A` itself.
|
SimpleGraph.adjMatrix_mulVec_apply
theorem SimpleGraph.adjMatrix_mulVec_apply :
∀ {V : Type u_1} {α : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : Fintype V]
[inst_2 : NonAssocSemiring α] (v : V) (vec : V → α),
(SimpleGraph.adjMatrix α G).mulVec vec v = (G.neighborFinset v).sum fun u => vec u
The theorem `SimpleGraph.adjMatrix_mulVec_apply` states that for any given simple graph `G` with vertices of type `V` and adjacency matrix with entries of type `α`, and for any function `vec` from `V` to `α`, the result of multiplying the adjacency matrix of `G` by `vec` at a vertex `v` is equal to the sum over all neighbors `u` of `v` of the values of `vec` at `u`. In other words, the product of the adjacency matrix and a vector at a certain vertex is the sum of the vector's values at the neighbors of that vertex. This involves the non-associative semiring structure of `α`, as well as the finite type structure of `V`, and the decidable relation of adjacency in `G`.
More concisely: For any simple graph with finite vertex set and adjacency matrix over a non-associative semiring, the product of the adjacency matrix and a vector at a vertex equals the sum of the vector values over its neighboring vertices.
|
SimpleGraph.toGraph_adjMatrix_eq
theorem SimpleGraph.toGraph_adjMatrix_eq :
∀ {V : Type u_1} (α : Type u_2) (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : MulZeroOneClass α]
[inst_2 : Nontrivial α], ⋯.toGraph = G
The theorem `SimpleGraph.toGraph_adjMatrix_eq` states that for any type `V`, any type `α`, and any simple graph `G` over `V`, given that the adjacency relation of `G` is decidable, and `α` forms a multiplication-zero-one class and is nontrivial, the graph that is induced by the adjacency matrix of `G` is `G` itself. In simpler terms, the graph we get when we construct it from `G`'s adjacency matrix is the same as `G`.
More concisely: Given a simple graph G over type V with decidable adjacency relation, and type α forming a multiplication-zero-one class and being nontrivial, the graph induced from G's adjacency matrix is equal to G.
|
SimpleGraph.isAdjMatrix_adjMatrix
theorem SimpleGraph.isAdjMatrix_adjMatrix :
∀ {V : Type u_1} (α : Type u_2) (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : Zero α] [inst_2 : One α],
(SimpleGraph.adjMatrix α G).IsAdjMatrix
The theorem `SimpleGraph.isAdjMatrix_adjMatrix` affirms that for any type `V`, any type `α` with defined `Zero` and `One` instances, and any simple graph `G` with vertices of type `V` and a decidable adjacency relation `G.Adj`, the adjacency matrix defined by `SimpleGraph.adjMatrix α G` is indeed an adjacency matrix. Here, an adjacency matrix is a square matrix that represents the adjacency relation of a finite graph, with the entries being `1` (from the `One α` instance) when two vertices are adjacent, and `0` (from the `Zero α` instance) otherwise.
More concisely: Given a simple graph with decidable adjacency relation and vertices of type `V` in Lean 4, the `SimpleGraph.adjMatrix α G` matrix represents the adjacency relation, where entry `(i, j)` equals `One α` if vertices `i` and `j` are adjacent, and `Zero α` otherwise.
|