Mathlib.Combinatorics.SimpleGraph.Clique._auxLemma.52
theorem Mathlib.Combinatorics.SimpleGraph.Clique._auxLemma.52 :
∀ {α : Type u} {a : α} {s : Set α}, ({a} ⊆ s) = (a ∈ s)
This theorem states that for any type `α`, any element `a` of type `α`, and any set `s` of elements of type `α`, the statement "the set containing only `a` is a subset of `s`" is equivalent to "element `a` is a member of set `s`". In mathematical terms, we can express this as: for all `α`, `a`, and `s`, `{a} ⊆ s` if and only if `a ∈ s`.
More concisely: For any type `α`, set `s` of elements from `α`, and `a` an element of `α`, the sets `{a}` and `s` are equal as sets if and only if `a` is an element of `s`.
|
SimpleGraph.CliqueFree.replaceVertex
theorem SimpleGraph.CliqueFree.replaceVertex :
∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ} [inst : DecidableEq α],
G.CliqueFree n → ∀ (s t : α), (G.replaceVertex s t).CliqueFree n
This theorem asserts that for any type `α`, any simple graph `G` of type `α`, any natural number `n`, and any instances of decidable equality on `α`, if the graph `G` is $n$-clique-free, then the graph obtained by replacing a vertex `s` with a vertex `t` in graph `G` is also $n$-clique-free. In other words, the property of being $n$-clique-free is preserved under the operation of `replaceVertex` in a `SimpleGraph`.
More concisely: If `G` is an `n`-clique-free simple graph of type `α` and `s` and `t` are vertices in `α`, then the graph obtained by replacing `s` with `t` in `G` is also `n`-clique-free.
|
Mathlib.Combinatorics.SimpleGraph.Clique._auxLemma.19
theorem Mathlib.Combinatorics.SimpleGraph.Clique._auxLemma.19 :
∀ {α : Type u_1} {G : SimpleGraph α} {s : Finset α} [inst : DecidableEq α],
G.IsNClique 3 s = ∃ a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}
The theorem `Mathlib.Combinatorics.SimpleGraph.Clique._auxLemma.19` states that for any type `α`, any Simple Graph `G` of `α`, and any finite set `s` of `α` with decidable equality, the statement that `s` forms a 3-clique in `G` is equivalent to the existence of three distinct elements `a`, `b`, and `c` in `α` such that `a` is adjacent to both `b` and `c`, `b` is also adjacent to `c`, and `s` is the set containing exactly `a`, `b`, and `c`. In graph theory, a 3-clique is a set of three vertices that are all connected to each other.
More concisely: For any Simple Graph `G` of type `α` and finite decidably-equaled set `s` of `α`, `s` forms a 3-clique in `G` if and only if there exist distinct elements `a, b, c` in `α` such that `a` is adjacent to both `b` and `c`, `b` is adjacent to `c`, and `s = {a, b, c}` .
|
Mathlib.Combinatorics.SimpleGraph.Clique._auxLemma.7
theorem Mathlib.Combinatorics.SimpleGraph.Clique._auxLemma.7 :
∀ {α : Type u_1} (G : SimpleGraph α) {n : ℕ} {s : Finset α}, G.IsNClique n s = (G.IsClique ↑s ∧ s.card = n) := by
sorry
The theorem `_auxLemma.7` states that for any simple graph `G` of type `α`, and for any finite set `s` of vertices in `G` and a natural number `n`, the predicate `IsNClique G n s` holds true if and only if two conditions are met: firstly, `s` is a clique in `G` (meaning that every pair of distinct vertices in `s` are adjacent in `G`), and secondly, the number of vertices in the set `s` equals `n`. In other words, `s` is a clique of size `n` in the graph `G`.
More concisely: A finite subset of vertices in a simple graph is a clique of size n if and only if it is a clique and has exactly n elements.
|
SimpleGraph.cliqueFree_of_card_lt
theorem SimpleGraph.cliqueFree_of_card_lt :
∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ} [inst : Fintype α], Fintype.card α < n → G.CliqueFree n
This theorem, `SimpleGraph.cliqueFree_of_card_lt`, states that for any type `α`, any simple graph `G` of type `α`, and any natural number `n`, given that `α` is a finite type (i.e., there exists a finite number of elements of type `α`), if the number of elements in `α` is less than `n`, then the graph `G` is `n`-clique free. In other words, the graph `G` does not contain any complete subgraph with `n` vertices. A tighter bound for this theorem can be found in `SimpleGraph.cliqueFree_of_chromaticNumber_lt`.
More concisely: For any finite type `α` and simple graph `G` of type `α`, if the number of elements in `α` is less than the number `n`, then `G` has no complete subgraph with `n` vertices.
|
Mathlib.Combinatorics.SimpleGraph.Clique._auxLemma.21
theorem Mathlib.Combinatorics.SimpleGraph.Clique._auxLemma.21 :
∀ {α : Type u_1} (G : SimpleGraph α) {s : Set α}, G.IsClique s = (SimpleGraph.induce s G = ⊤)
This theorem states that for any given type `α`, a simple graph `G` of that type, and a set `s` of that type, the set `s` is a clique in the graph `G` if and only if when the graph `G` is restricted to the vertices in the set `s` (i.e., all edges incident to vertices outside the set are deleted), the resulting graph is a complete graph (denoted by `⊤`). Here, a clique is defined as a set of vertices that are pairwise adjacent, and a complete graph is a simple undirected graph in which every pair of distinct vertices is connected by a unique edge.
More concisely: A set `s` of type `α` is a clique in the simple graph `G` of type `α` if and only if the subgraph of `G` induced by `s` is a complete graph.
|
SimpleGraph.CliqueFree.cliqueSet
theorem SimpleGraph.CliqueFree.cliqueSet :
∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ}, G.CliqueFree n → G.cliqueSet n = ∅
This theorem states that for any simple graph `G` of a certain type `α` and any natural number `n`, if `G` is `n`-clique-free (that is, it does not contain any complete subgraph of size `n`), then the set of all `n`-cliques in `G` is empty. In graph theory, a clique is a subset of vertices of an undirected graph such that every two distinct vertices in the clique are adjacent; and an `n`-clique refers to a clique that contains `n` vertices.
More concisely: If `G` is a simple graph of type `α` that is `n`-clique-free, then the set of `n`-cliques in `G` is empty.
|
SimpleGraph.IsNClique.mono
theorem SimpleGraph.IsNClique.mono :
∀ {α : Type u_1} {G H : SimpleGraph α} {n : ℕ} {s : Finset α}, G ≤ H → G.IsNClique n s → H.IsNClique n s
This theorem states that for any two simple graphs `G` and `H` of type `α`, a natural number `n`, and a finite set `s` of type `α`, if `G` is a subgraph of `H` (`G ≤ H`) and `s` is an `n`-clique in `G` (`SimpleGraph.IsNClique G n s`), then `s` is also an `n`-clique in `H` (`SimpleGraph.IsNClique H n s`). In other words, an `n`-clique in a subgraph remains an `n`-clique in the supergraph.
More concisely: If `G` is a subgraph of `H` and `s` is an `n`-clique in `G`, then `s` is an `n`-clique in `H`.
|
SimpleGraph.IsClique.subsingleton
theorem SimpleGraph.IsClique.subsingleton : ∀ {α : Type u_1} {s : Set α}, ⊥.IsClique s → s.Subsingleton
This theorem states that for any type `α` and any set `s` of that type, if the bottom simple graph (`⊥`) is a clique on `s`, then `s` is a subsingleton. In other words, if every two distinct vertices in `s` are adjacent in the bottom simple graph, then `s` can contain at most one element.
More concisely: If `α` is a type and `s` is a set of distinct elements of `α` such that every pair of elements in `s` is related by the bottom relation, then `s` has at most one element.
|
SimpleGraph.CliqueFree.cliqueFinset
theorem SimpleGraph.CliqueFree.cliqueFinset :
∀ {α : Type u_1} {G : SimpleGraph α} [inst : Fintype α] [inst_1 : DecidableEq α] [inst_2 : DecidableRel G.Adj]
{n : ℕ}, G.CliqueFree n → G.cliqueFinset n = ∅
The theorem `SimpleGraph.CliqueFree.cliqueFinset` asserts that for any type `α`, any simple graph `G` of type `α`, where `α` is a finite type and has decidable equality, and the adjacency relation `Adj` of `G` is decidable, and for any natural number `n`, if the graph `G` is `n`-clique-free (i.e. there are no cliques of size `n`), then the finset of `n`-cliques of the graph `G` is empty. In other words, if a graph doesn't have any cliques of size `n`, then there are no `n`-cliques to list in the finset of `n`-cliques.
More concisely: If `α` is a finite type with decidable equality, `G` is a simple graph of type `α` with decidable adjacency relation and `n` natural number, then `G` being `n`-clique-free implies the empty finset of `n`-cliques for `G`.
|
Mathlib.Combinatorics.SimpleGraph.Clique._auxLemma.8
theorem Mathlib.Combinatorics.SimpleGraph.Clique._auxLemma.8 : ∀ {α : Sort u_1} {a b : α}, (a = b) = (b = a)
This theorem states that for all types `α` and any two elements `a` and `b` of type `α`, the proposition `a = b` is equivalent to `b = a`. In other words, equality is symmetric: if `a` equals `b`, then `b` equals `a`.
More concisely: For all types `α` and all elements `a` and `b` of type `α`, the proposition `a = b` is equivalent to `b = a`. (Or more succinctly: Equality is a symmetric relation.)
|
SimpleGraph.cliqueFree_completeMultipartiteGraph
theorem SimpleGraph.cliqueFree_completeMultipartiteGraph :
∀ {n : ℕ} {ι : Type u_3} [inst : Fintype ι] (V : ι → Type u_4),
Fintype.card ι < n → (SimpleGraph.completeMultipartiteGraph V).CliqueFree n
The theorem `SimpleGraph.cliqueFree_completeMultipartiteGraph` states that for any natural number `n`, any index type `ι` with a finiteness property, and any family of vertex types `V` indexed by `ι`, if the number of elements in `ι` is less than `n`, then the complete multipartite graph constructed over `V` is `n`-clique-free. In terms of graph theory, this means that a complete `r`-partite graph (where `r` is the number of elements in `ι`) does not contain any fully connected subgraph (or `n`-clique) when `r` is less than `n`.
More concisely: For any natural number `n`, any finite index type `ι` with `|ι| < n`, and any complete `r`-partite graph constructed over a family of vertex types indexed by `ι`, there is no `n`-clique present in the graph when `r < n`.
|
SimpleGraph.isClique_iff_induce_eq
theorem SimpleGraph.isClique_iff_induce_eq :
∀ {α : Type u_1} (G : SimpleGraph α) {s : Set α}, G.IsClique s ↔ SimpleGraph.induce s G = ⊤
This theorem states that for any simple graph `G` and a set of vertices `s` from the graph, `s` is a clique of `G` if and only if the graph obtained by restricting `G` to the vertices in `s` and deleting all edges incident to vertices outside `s` is a complete graph. In other words, a subset of vertices `s` forms a clique in a graph `G` exactly when every pair of distinct vertices in `s` is connected by an edge in the induced subgraph.
More concisely: A subset of vertices in a simple graph forms a clique if and only if the induced subgraph is a complete graph.
|
Mathlib.Combinatorics.SimpleGraph.Clique._auxLemma.54
theorem Mathlib.Combinatorics.SimpleGraph.Clique._auxLemma.54 :
∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ} {s : Finset α}, (s ∈ G.cliqueSet n) = G.IsNClique n s
The theorem `Mathlib.Combinatorics.SimpleGraph.Clique._auxLemma.54` states that for any type `α`, graph `G` of type `SimpleGraph α`, natural number `n`, and finite set `s` of type `Finset α`, the set `s` is in the `n`-cliques of the graph `G` (i.e., `s ∈ SimpleGraph.cliqueSet G n`) if and only if `s` is an `n`-clique in the graph `G` (i.e., `SimpleGraph.IsNClique G n s`). Essentially, it connects the concept of a set being in the `n`-cliques of a graph to the set being an `n`-clique of the graph.
More concisely: For any type `α`, graph `G` of type `SimpleGraph α`, natural number `n`, and finite set `s` of type `Finset α`, the set `s` is an `n`-clique in the graph `G` if and only if it is in the set of `n`-cliques of `G`.
|
SimpleGraph.CliqueFree.comap
theorem SimpleGraph.CliqueFree.comap :
∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {n : ℕ} {H : SimpleGraph β},
H.Embedding G → G.CliqueFree n → H.CliqueFree n
This theorem states that for any two types `α` and `β`, and any simple graphs `G` of type `α` and `H` of type `β`, if `H` can be embedded into `G`, and if `G` is clique-free of order `n`, then `H` is also clique-free of order `n`. In other words, if a graph `G` does not contain any complete subgraph of `n` vertices, then any graph that can be mapped into `G` without any collisions also does not contain such a complete subgraph.
More concisely: If two simple graphs `G` and `H` are such that `H` is embeddable into `G` and `G` is clique-free of order `n`, then `H` is also clique-free of order `n`.
|
Mathlib.Combinatorics.SimpleGraph.Clique._auxLemma.20
theorem Mathlib.Combinatorics.SimpleGraph.Clique._auxLemma.20 :
∀ {V : Type u} {G : SimpleGraph V} {u : V} (p : G.Walk u u),
p.IsCycle = (p.IsTrail ∧ p ≠ SimpleGraph.Walk.nil ∧ p.support.tail.Nodup)
This theorem, `Mathlib.Combinatorics.SimpleGraph.Clique._auxLemma.20`, states that for any given type `V`, a simple graph `G` of type `V`, and a vertex `u` of type `V`, a walk `p` from vertex `u` back to `u` in the graph `G` is a cycle if and only if the walk `p` is a trail (meaning that no edges are repeated), the walk `p` is not an empty walk, and the list of vertices visited in the walk `p` (excluding the first vertex), which is obtained by first getting the support of the walk `p` and then taking the tail of this list, has no duplicate vertices. In other words, a walk in a simple graph is a cycle if it is a trail, it is not an empty walk, and it visits no vertex more than once (except for the starting/ending vertex).
More concisely: A simple graph walk is a cycle if and only if it is a trail, non-empty, and visits each vertex at most once (excluding the starting/ending vertex).
|
Mathlib.Combinatorics.SimpleGraph.Clique._auxLemma.37
theorem Mathlib.Combinatorics.SimpleGraph.Clique._auxLemma.37 : ∀ {α : Sort u_1} (a b : α), (¬a = b) = (a ≠ b) := by
sorry
This theorem states that for any type `α` and any two elements `a` and `b` of this type, the proposition "it is not the case that `a` is equal to `b`" is logically equivalent to " `a` is not equal to `b`". In other words, the logical negation of equality (`¬a = b`) is equivalent to the inequality (`a ≠ b`). This is a basic property of equality in logic.
More concisely: The logical negation of `a = b` is equivalent to `a ≠ b` for any type `α` and elements `a` and `b` of type `α`.
|