Revision #1639 → #2148 · back to history
modifiedTree (lead)f92004116533
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | SimpleGraph.isTree_iff_existsUnique_path |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Combinatorics.SimpleGraph.Acyclic |
| note | — | `isTree_iff_existsUnique_path` states a graph is a tree iff the vertex type is nonempty and every pair of vertices is joined by a unique path. |
| status | — | formalized |
modifiedForest (lead)d1928f7c8c68
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | SimpleGraph.isAcyclic_iff_path_unique |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Combinatorics.SimpleGraph.Acyclic |
| note | — | `IsAcyclic` is defined as having no cycles, and `isAcyclic_iff_path_unique` characterizes a forest as having at most one path between any two vertices. |
| status | — | formalized |
modifiedPolytree / directed tree06769a282cd3
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | Quiver.Arborescence |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.Combinatorics.Quiver.Arborescence |
| note | — | Mathlib formalizes the rooted directed-tree (arborescence) variant via `Quiver.Arborescence`, but not the general polytree (DAG whose underlying graph is a tree). |
| status | — | partial |
modifiedPolyforest155825ccd046
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No definition of a polyforest (DAG whose underlying graph is a forest) was found in Mathlib. |
| status | — | not_formalized |
modifiedRooted tree, arborescence, anti-arborescence7cc541e20dd0
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | Quiver.Arborescence |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.Combinatorics.Quiver.Arborescence |
| note | — | `Quiver.Arborescence` formalizes an arborescence (unique path from root to every vertex), but anti-arborescences and the general undirected-rooted-tree notion are not formalized. |
| status | — | partial |
modifiedRooted forest, branching, anti-branching4ea4bed8eab7
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No notion of rooted forest, branching, or anti-branching was found in Mathlib. |
| status | — | not_formalized |
modifiedTree (equivalent conditions)3ff3d03ab674
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | SimpleGraph.isTree_iff_existsUnique_path |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Combinatorics.SimpleGraph.Acyclic |
| note | — | Several equivalences are proved: `isTree_iff_existsUnique_path`, `isTree_iff_minimal_connected`, `maximal_isAcyclic_iff_isTree`, and `isTree_iff_maximal_isAcyclic`. |
| status | — | formalized |
modifiedFinite tree equivalent conditions0fd33a883db2
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | SimpleGraph.isTree_iff_connected_and_card |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Combinatorics.SimpleGraph.Acyclic |
| note | — | `isTree_iff_connected_and_card` proves that, over a finite vertex type, a graph is a tree iff it is connected and has exactly `n - 1` edges. |
| status | — | formalized |
modifiedOrder-zero graph as forestfd7b0a00ed3a
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | SimpleGraph.isAcyclic_bot |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.Combinatorics.SimpleGraph.Acyclic |
| note | — | `isAcyclic_bot` shows the empty graph is acyclic, and `IsTree` requires `Connected` (hence Nonempty V), so the convention is implicitly captured but not articulated as such. |
| status | — | partial |
modifiedInternal, external, branch vertexe63e4a78d7b7
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib has `SimpleGraph.degree` but no named predicates for internal/external/branch vertices. |
| status | — | not_formalized |
modifiedIrreducible tree94d0291b7d53
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No notion of irreducible/series-reduced tree was found in Mathlib. |
| status | — | not_formalized |
modifiedForest567260d4d42c
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | SimpleGraph.IsAcyclic |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Combinatorics.SimpleGraph.Acyclic |
| note | — | `IsAcyclic` is defined directly as having no cyclic walk; `IsAcyclic.isTree_connectedComponent` shows the disjoint-union-of-trees view. |
| status | — | formalized |
modifiedCounting trees in a forest845dd46f0eff
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Mathlib has `IsTree.card_edgeFinset` (n = m+1 for a tree) but no theorem expressing #components = #vertices − #edges for a forest. |
| status | — | not_formalized |
modifiedPolytree448aea9d1cf4
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | Quiver.Arborescence |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.Combinatorics.Quiver.Arborescence |
| note | — | Only the rooted/arborescence special case appears in Mathlib; the general polytree (DAG whose underlying graph is a tree) is not formalized. |
| status | — | partial |
modifiedPolyforestbf86be210ebf
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No definition of polyforest was found in Mathlib. |
| status | — | not_formalized |
modifiedRooted tree, arborescence, in-treea59cfd24f796
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | Quiver.Arborescence |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.Combinatorics.Quiver.Arborescence |
| note | — | `Quiver.Arborescence` covers out-arborescences from a root; in-trees and a generic undirected-graph + designated-root rooted tree are not formalized. |
| status | — | partial |
modifiedTree-order7be5b5222189
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | IsPredArchimedean.findAtom |
| mathlib.match_kind | — | generalization |
| mathlib.module | — | Mathlib.Order.SuccPred.Tree |
| note | — | `Mathlib.Order.SuccPred.Tree` models a rooted tree as a `PartialOrder` with `PredOrder`+`IsPredArchimedean`+`OrderBot`, encoding the tree-order, but it is not connected to `SimpleGraph` trees. |
| status | — | partial |
modifiedNormal treeec52a7a1a5cf
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No notion of normal tree was found in Mathlib. |
| status | — | not_formalized |
modifiedFree treee5326b5ba439
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | SimpleGraph.IsTree |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Combinatorics.SimpleGraph.Acyclic |
| note | — | `SimpleGraph.IsTree` is a connected acyclic graph with no designated root, matching the notion of a free tree. |
| status | — | formalized |
modifiedLabeled treeaa1d1fb3cd7e
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No labeled-tree concept beyond the implicit vertex-type indexing was found in Mathlib. |
| status | — | not_formalized |
modifiedRecursive treeab371879bca1
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No recursive-tree definition was found in Mathlib. |
| status | — | not_formalized |
modifiedParent, child, ascendant, descendant, sibling, leaf931f529346ba
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | BinaryTree |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.Data.Tree.Basic |
| note | — | `BinaryTree` (and `Order.SuccPred.Tree` via `Order.pred`) encode parent/child relations in their respective settings, but Mathlib has no graph-theoretic parent/child/leaf API for `SimpleGraph` rooted trees. |
| status | — | partial |
modifiedHeight and depthc7a8dedde557
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | BinaryTree.height |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.Data.Tree.Basic |
| note | — | `BinaryTree.height` defines tree height for the binary-tree datatype only; no graph-theoretic height/depth on `SimpleGraph` rooted trees was found. |
| status | — | partial |
modifiedk-ary tree, binary tree, ternary tree681c7cb7342f
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | BinaryTree |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.Data.Tree.Basic |
| note | — | Mathlib formalizes `BinaryTree` as a recursive datatype, but no general k-ary or ternary tree predicate over graphs is provided. |
| status | — | partial |
modifiedOrdered (plane) treec1118fd1c822
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No ordered/plane-tree definition was found in Mathlib. |
| status | — | not_formalized |
modifiedEvery tree is bipartite363dc88d5d12
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | SimpleGraph.IsTree.isBipartite |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Combinatorics.SimpleGraph.Acyclic |
| note | — | `IsTree.isBipartite` (via the explicit two-coloring `IsTree.coloringTwo`) proves every tree is bipartite. |
| status | — | formalized |
modifiedCountable trees are planar1f28cc7bf663
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Planarity of graphs is not formalized in Mathlib (only mentioned in a docstring). |
| status | — | not_formalized |
modifiedSpanning tree existencedd2801e07a61
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | SimpleGraph.Connected.exists_isTree_le |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Combinatorics.SimpleGraph.Acyclic |
| note | — | `Connected.exists_isTree_le` proves every connected graph has a spanning subgraph that is a tree. |
| status | — | formalized |
addedTrémaux tree existence9f313b3235f7
modifiedLeaves in finite treesb7d62b1cb34b
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | SimpleGraph.IsTree.exists_vert_degree_one_of_nontrivial |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.Combinatorics.SimpleGraph.Acyclic |
| note | — | `IsTree.exists_vert_degree_one_of_nontrivial` gives the existence of one degree-1 vertex (one leaf), but the stronger "at least two leaves" statement was not found. |
| status | — | partial |
modifiedTree as median graph40b6b756ad01
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No median-graph or Steiner-point property of trees was found in Mathlib. |
| status | — | not_formalized |
modifiedCenter and centroid of a treeca06104a4649
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No notion of graph center/centroid for trees was found in Mathlib. |
| status | — | not_formalized |
modifiedMaximal cliques of a tree0ce0261d2217
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Although Mathlib has `SimpleGraph.IsClique`, the specific characterization of maximal cliques of a tree was not found. |
| status | — | not_formalized |
modifiedCayley's formulacc548c4e205a
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | Cayley's formula counting labeled trees by n^{n-2} was not found in Mathlib. |
| status | — | not_formalized |
modifiedMatrix tree theorem575bf00db0bc
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | `LapMatrix` defines the graph Laplacian and proves rank-related results, but Kirchhoff's matrix-tree theorem (cofactor counts spanning trees) was not found. |
| status | — | not_formalized |
modifiedOtter's asymptotic estimate (unlabeled trees)79684904bdaf
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No asymptotic count of unlabeled trees (Otter's theorem) was found in Mathlib. |
| status | — | not_formalized |
modifiedOtter's asymptotic estimate (rooted trees)97aab062df30
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No asymptotic count of rooted unlabeled trees was found in Mathlib. |
| status | — | not_formalized |
modifiedPath graph6489402948b9
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | SimpleGraph.pathGraph |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Combinatorics.SimpleGraph.Hasse |
| note | — | `SimpleGraph.pathGraph n` is the path graph on `Fin n`, with adjacency and connectedness lemmas. |
| status | — | formalized |
modifiedStarlike treebd1471703b39
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No starlike-tree definition was found in Mathlib. |
| status | — | not_formalized |
modifiedStar tree6deb175514f2
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | SimpleGraph.starGraph |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Combinatorics.SimpleGraph.Star |
| note | — | `SimpleGraph.starGraph r` is the star graph centered at `r`, and `isTree_starGraph` proves it is a tree. |
| status | — | formalized |
modifiedCaterpillar treeeaf6a613a0a0
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No caterpillar-tree definition was found in Mathlib. |
| status | — | not_formalized |
modifiedLobster treec8833899be06
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No lobster-tree definition was found in Mathlib. |
| status | — | not_formalized |
modifiedRegular tree / Bethe lattice873f5be5a3bc
| Field | From #1639 | To #2148 |
|---|
| mathlib.decl | — | — |
| mathlib.match_kind | — | — |
| mathlib.module | — | — |
| note | — | No regular-tree or Bethe-lattice definition was found in Mathlib. |
| status | — | not_formalized |