SimpleGraph.le_minDegree_of_forall_le_degree
theorem SimpleGraph.le_minDegree_of_forall_le_degree :
∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] [inst_2 : Nonempty V] (k : ℕ),
(∀ (v : V), k ≤ G.degree v) → k ≤ G.minDegree
This theorem states that in a non-empty graph, if a natural number 'k' is less than or equal to the degree of every vertex in the graph, then 'k' is also less than or equal to the minimum degree of the graph. Here, the graph is represented by a SimpleGraph structure 'G', and 'degree' and 'minDegree' are functions that calculate the degree of a single vertex and the minimum degree in the graph respectively. The theorem assumes that the graph is finite (Fintype V) and that the adjacency relation (G.Adj) is decidable, meaning that for any two vertices, it can be determined whether or not they are connected. The condition that the graph is nonempty is necessary because the minimum degree 'G.minDegree' is defined to be a natural number.
More concisely: In a finite, non-empty SimpleGraph where the degree of every vertex is less than or equal to a natural number 'k', the minimum degree of the graph is also less than or equal to 'k'.
|
SimpleGraph.card_neighborSet_eq_degree
theorem SimpleGraph.card_neighborSet_eq_degree :
∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)],
Fintype.card ↑(G.neighborSet v) = G.degree v
The theorem `SimpleGraph.card_neighborSet_eq_degree` states that for any simple graph `G` and any vertex `v` in `G`, provided that the set of neighboring vertices of `v` is finite (`Fintype`), the cardinality of the set of neighboring vertices (`Fintype.card ↑(SimpleGraph.neighborSet G v)`) is equal to the degree of the vertex `v` in the graph (`SimpleGraph.degree G v`). The degree of a vertex in a simple graph is the number of vertices adjacent to it, and the neighbor set of a vertex is the set of its adjacent vertices, so this theorem essentially states that the number of elements in the neighbor set of a vertex is equal to the degree of the vertex.
More concisely: For any simple graph and vertex with a finite set of neighbors, the cardinality of the neighbor set equals the degree of the vertex.
|
SimpleGraph.card_edgeFinset_top_eq_card_choose_two
theorem SimpleGraph.card_edgeFinset_top_eq_card_choose_two :
∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V], ⊤.edgeFinset.card = (Fintype.card V).choose 2 := by
sorry
This theorem states that the complete graph on `n` vertices has `n.choose 2` edges. Here, `V` represents the set of vertices and is assumed to be a finite type (`Fintype V`). `DecidableEq V` means that equality between two vertices can be definitively determined. The notation `⊤.edgeFinset.card` represents the number of edges in the complete graph on `V`, and `(Fintype.card V).choose 2` is the binomial coefficient "n choose 2", which corresponds to the number of ways to choose 2 elements from a set of `n` elements. Thus, the theorem asserts that the number of edges in a complete graph with `n` vertices is equal to the number of ways to choose 2 vertices from the `n` vertices, which is what is expected in a complete graph since every pair of distinct vertices is connected by an edge.
More concisely: The complete graph on a finite set of `n` vertices has `n choose 2` edges.
|
SimpleGraph.exists_minimal_degree_vertex
theorem SimpleGraph.exists_minimal_degree_vertex :
∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] [inst_2 : Nonempty V],
∃ v, G.minDegree = G.degree v
The theorem `SimpleGraph.exists_minimal_degree_vertex` states that for any Simple Graph `G` with vertex type `V`, given that `V` is a finite type, the adjacency relation of `G` is decidable, and `V` is non-empty, there exists a vertex `v` such that the minimal degree of `G` is equal to the degree of `v`. In other words, in every non-empty finite simple graph, there exists at least one vertex with the minimal degree.
More concisely: In every non-empty finite simple graph, there exists a vertex with the minimum degree.
|
SimpleGraph.edgeFinset_strict_mono
theorem SimpleGraph.edgeFinset_strict_mono :
∀ {V : Type u_1} {G₁ G₂ : SimpleGraph V} [inst : Fintype ↑G₁.edgeSet] [inst_1 : Fintype ↑G₂.edgeSet],
G₁ < G₂ → G₁.edgeFinset ⊂ G₂.edgeFinset
The theorem `SimpleGraph.edgeFinset_strict_mono` states that for any two Simple Graphs `G₁` and `G₂` of type `V` with finite edge sets, if `G₁` is strictly smaller than `G₂` (meaning `G₂` has at least one edge that `G₁` doesn't), then the edge set (represented as a finite set or `Finset`) of `G₁` is strictly subset of the edge set of `G₂`. In other words, all edges in `G₁` are also in `G₂`, but there's at least one edge in `G₂` not in `G₁`.
More concisely: If two simple graphs of finite edge sets `G₁` and `G₂` have `G₁` strictly contained as a subgraph of `G₂`, then the edge set of `G₁` is a strict subset of the edge set of `G₂`.
|
SimpleGraph.card_edgeFinset_le_card_choose_two
theorem SimpleGraph.card_edgeFinset_le_card_choose_two :
∀ {V : Type u_1} {G : SimpleGraph V} [inst : Fintype ↑G.edgeSet] [inst_1 : Fintype V],
G.edgeFinset.card ≤ (Fintype.card V).choose 2
This theorem states that for any given graph 'G' with vertex set 'V', the number of edges in 'G' is at most the binomial coefficient "n choose 2", where 'n' is the number of vertices in 'V'. This is a consequence of the fact that any pair of distinct vertices can contribute at most one edge, and there are "n choose 2" such pairs in a graph with 'n' vertices.
More concisely: The number of edges in a graph with n vertices is at most n choose 2.
|
SimpleGraph.edgeFinset_mono
theorem SimpleGraph.edgeFinset_mono :
∀ {V : Type u_1} {G₁ G₂ : SimpleGraph V} [inst : Fintype ↑G₁.edgeSet] [inst_1 : Fintype ↑G₂.edgeSet],
G₁ ≤ G₂ → G₁.edgeFinset ⊆ G₂.edgeFinset
The theorem `SimpleGraph.edgeFinset_mono` states that for any two simple graphs `G₁` and `G₂` of vertices of type `V`, where both `G₁.edgeSet` and `G₂.edgeSet` have a finite number of elements, if `G₁` is a subgraph of `G₂` (denoted as `G₁ ≤ G₂`), then the finite set of edges of `G₁` is a subset of the finite set of edges of `G₂`. In other words, all edges present in the smaller graph are also present in the larger graph.
More concisely: If simple graphs $G\_1$ and $G\_2$ have finite edge sets, and $G\_1$ is a subgraph of $G\_2$, then the edge set of $G\_1$ is a subset of the edge set of $G\_2$.
|
SimpleGraph.minDegree_le_degree
theorem SimpleGraph.minDegree_le_degree :
∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] (v : V),
G.minDegree ≤ G.degree v
This theorem states that for any graph `G` represented as a `SimpleGraph` over some type `V`, where `V` is a finite type and the adjacency relation `G.Adj` is a decidable relation, the minimum degree of the graph `G` is less than or equal to the degree of any given vertex `v` in the graph. In mathematical terms, if `G` is a finite simple graph and `v` is any vertex in `G`, then the minimum degree of `G` (i.e., the smallest number of edges connected to a vertex) is always less than or equal to the degree of `v` (i.e., the number of edges connected to `v`).
More concisely: For any finite simple graph G and vertex v, the minimum degree of G is less than or equal to the degree of v.
|
Mathlib.Combinatorics.SimpleGraph.Finite._auxLemma.3
theorem Mathlib.Combinatorics.SimpleGraph.Finite._auxLemma.3 :
∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)] (w : V),
(w ∈ G.neighborFinset v) = G.Adj v w
This theorem states that for any vertex 'v' of a simple graph 'G', where the set of vertices adjacent to 'v' (the neighbor set of 'v') is finite, a vertex 'w' belongs to the finite version (Finset) of this neighbor set if and only if 'v' is adjacent to 'w' in the graph 'G'. In other words, 'w' is in the finite neighbor set of 'v' precisely when 'w' and 'v' share an edge in 'G'. The adjacency relationship is defined by the function 'G.Adj'.
More concisely: For any simple graph G and vertex v with finite neighbor set, vertex w is in v's neighbor set if and only if (v, w) is an edge in G.
|
SimpleGraph.maxDegree_le_of_forall_degree_le
theorem SimpleGraph.maxDegree_le_of_forall_degree_le :
∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] (k : ℕ),
(∀ (v : V), G.degree v ≤ k) → G.maxDegree ≤ k
This theorem states that in a simple graph, if a natural number `k` is greater than or equal to the degree of every vertex, then `k` is also greater than or equal to the maximum degree of the graph. A simple graph is defined by a set of vertices `V` and an adjacency relation `Adj` that's decidable. The degree of a vertex is the number of edges connected to it, while the maximum degree of the graph is the highest degree among all vertices in the graph.
More concisely: In a simple graph, if the degree of every vertex is less than or equal to a natural number `k`, then the maximum degree of the graph is also less than or equal to `k`.
|
SimpleGraph.exists_maximal_degree_vertex
theorem SimpleGraph.exists_maximal_degree_vertex :
∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] [inst_2 : Nonempty V],
∃ v, G.maxDegree = G.degree v
The theorem `SimpleGraph.exists_maximal_degree_vertex` states that for any SimpleGraph `G` with vertex set `V`, under the conditions that `V` is a finite type, the adjacency relation of `G` is decidable, and `V` is nonempty, there exists a vertex `v` such that the maximum degree of `G` is equal to the degree of `v`. In other words, in any non-empty simple graph with a finite number of vertices and a decidable adjacency relation, there always exists a vertex that has the maximum degree.
More concisely: In any finite, non-empty simple graph with a decidable adjacency relation, there exists a vertex of maximum degree.
|
SimpleGraph.Adj.card_commonNeighbors_lt_degree
theorem SimpleGraph.Adj.card_commonNeighbors_lt_degree :
∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {v w : V},
G.Adj v w → Fintype.card ↑(G.commonNeighbors v w) < G.degree v
This theorem, `SimpleGraph.Adj.card_commonNeighbors_lt_degree`, states that for any given finite simple graph `G` with vertices of type `V` and for any two vertices `v` and `w` in this graph such that `v` is adjacent to `w` (i.e., there is an edge between `v` and `w`), the number of common neighbors that `v` and `w` share is strictly less than the degree of `v`. Here, the degree of a vertex is the number of edges connected to it, and a common neighbor of two vertices is a vertex that is adjacent to both of them. Note that the adjacency relation `G.Adj` is assumed to be decidable, meaning for any two vertices, it can be definitively determined whether there is an edge between them or not.
More concisely: For any finite simple graph G and vertices v and w with an edge between them, the number of common neighbors v and w share is strictly less than the degree of vertex v.
|
SimpleGraph.maxDegree_lt_card_verts
theorem SimpleGraph.maxDegree_lt_card_verts :
∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] [inst_2 : Nonempty V],
G.maxDegree < Fintype.card V
The theorem `SimpleGraph.maxDegree_lt_card_verts` states that for any simple graph `G` (a graph with no loops or multiple edges) over some finite, nonempty set of vertices `V`, the maximum degree of the graph is less than the number of vertices in `V`. Here, the degree of a vertex is the number of edges connected to it. The requirement that `V` is nonempty avoids a situation where we would be asserting the existence of a natural number less than zero. This theorem is quantified over all such graphs `G` and vertex sets `V`, and assumes that the adjacency relation `G.Adj` for the graph is decidable (i.e., for any two vertices, it's possible to decide whether or not they're adjacent in `G`).
More concisely: For any simple graph with finite, nonempty vertex set, the maximum degree of its vertices is less than the number of vertices.
|
SimpleGraph.degree_le_maxDegree
theorem SimpleGraph.degree_le_maxDegree :
∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] (v : V),
G.degree v ≤ G.maxDegree
This theorem states that for any vertex 'v' in a finite, undirected graph 'G' with vertices of type 'V', the degree of 'v' (the number of edges incident to 'v') is always less than or equal to the maximum degree of any vertex in the graph 'G'. The adjacency relation 'G.Adj' in the graph 'G' is decidable, meaning that for any two vertices, it can be definitively determined whether or not they are adjacent.
More concisely: For any vertex in a finite, undirected graph, the degree of that vertex is bounded by the maximum degree of any vertex in the graph.
|
SimpleGraph.mem_edgeFinset
theorem SimpleGraph.mem_edgeFinset :
∀ {V : Type u_1} {G : SimpleGraph V} {e : Sym2 V} [inst : Fintype ↑G.edgeSet], e ∈ G.edgeFinset ↔ e ∈ G.edgeSet
This theorem states that for any type `V`, any simple graph `G` of type `V`, and any edge `e` represented as an unordered pair from `Sym2 V`, given that the edge set of `G` is finite, the edge `e` belongs to the `edgeFinset` of the graph `G` if and only if `e` belongs to the `edgeSet` of the graph `G`.
In other words, an edge is in the finite set representation (or `Finset`) of the edges of a simple graph `G` if and only if it is in the set of edges of `G`. This theorem bridges the gap between the set of edges and the finite set of edges in a simple graph.
More concisely: For any simple graph with finite edge set `G` of type `V`, the edge set `edgeSet G` equals the finite set representation `edgeFinset G` of its edges.
|
SimpleGraph.DeleteFar.le_card_sub_card
theorem SimpleGraph.DeleteFar.le_card_sub_card :
∀ {V : Type u_1} {G : SimpleGraph V} {𝕜 : Type u_2} [inst : OrderedRing 𝕜] [inst_1 : Fintype (Sym2 V)]
[inst_2 : Fintype ↑G.edgeSet] {p : SimpleGraph V → Prop} {r : 𝕜},
G.DeleteFar p r →
∀ ⦃H : SimpleGraph V⦄ [inst_3 : DecidableRel H.Adj],
H ≤ G → p H → r ≤ ↑G.edgeFinset.card - ↑H.edgeFinset.card
This theorem, known as an alias of the forward direction of `SimpleGraph.deleteFar_iff`, states that for any types `V` and `𝕜`, a simple graph `G` on `V`, a property `p` of such graphs, and a value `r` from `𝕜`, if `G` is a "far deletion" with respect to `p` and `r`, then for any simple graph `H` on `V` (with a decidable adjacency relation) that is a subgraph of `G` and satisfies property `p`, the value `r` is less than or equal to the difference between the cardinality of the edge sets of `G` and `H`. In other words, the number of edges deleted from `G` to obtain `H` is at least `r` when `H` satisfies property `p`. This theorem is related to the concepts of graph theory.
More concisely: If $G$ is a simple graph on $V$ with decidable adjacency relation, $p$ is a property of simple graphs, $r \in \mathbb{N}$, and $H$ is a subgraph of $G$ satisfying $p$, then the number of edges deleted from $G$ to obtain $H$ is at least $r$ if $G$ is a "far deletion" with respect to $p$ and $r$.
|
SimpleGraph.neighborFinset_eq_filter
theorem SimpleGraph.neighborFinset_eq_filter :
∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] {v : V} [inst_1 : DecidableRel G.Adj],
G.neighborFinset v = Finset.filter (G.Adj v) Finset.univ
This theorem states that for any simple graph `G` with vertices of a certain type `V`, which has a finite number of elements, and for any vertex `v` from `V`, if the adjacency relation `G.Adj` is decidable, then the finite set of neighbours of `v` in `G` is equal to the set of all vertices in `G` that satisfy the adjacency relation with `v`. In other words, the set of neighbours of `v` is the set of all vertices that are adjacent to `v` in the graph `G`.
More concisely: If `G` is a finite simple graph with decidable adjacency relation, then for any vertex `v` in `G`, the set of neighbours of `v` equals the set of vertices adjacent to `v` in `G`.
|