Basic

📁 Source: Mathlib/Combinatorics/Graph/Basic.lean

Statistics

Metric	Count
Definitions `Inc`, `other`, `IsLink`, `IsLoopAt`, `IsNonloopAt`, `edgeSet`, `incidenceSet`, `loopSet`, `vertexSet`, `«termE(_)»`»), `«termV(_)»`»)	11
Theorems `left_mem`, `right_mem`, `edge_mem`, `eq_of_isLink_of_ne_left`, `eq_or_eq_of_isLink`, `eq_or_eq_or_eq`, `inc_other`, `isLink_other`, `isLoopAt_or_isNonloopAt`, `vertex_mem`, `adj`, `edge_mem`, `eq_and_eq_or_eq_and_eq`, `inc_left`, `inc_right`, `isLink_iff`, `isLink_iff_eq`, `isLink_iff_sym2_eq`, `left_eq_of_right_ne`, `left_eq_or_eq`, `left_mem`, `left_unique`, `right_eq_or_eq`, `right_mem`, `right_unique`, `edge_mem`, `eq_of_inc`, `inc`, `not_isNonloopAt`, `vertex_mem`, `edge_mem`, `inc`, `not_isLoopAt`, `vertex_mem`, `adj_comm`, `edgeSet_eq_setOf_exists_isLink`, `edge_mem_iff_exists_isLink`, `eq_or_eq_of_isLink_of_isLink`, `exists_isLink_of_mem_edgeSet`, `ext`, `ext_iff`, `ext_inc`, `incidenceSet_subset_edgeSet`, `isLink_comm`, `isLink_iff_inc`, `isLink_self_iff`, `isLink_symm`, `isLoopAt_iff_inc_not_isNonloopAt`, `isNonloopAt_iff_inc_not_isLoopAt`, `left_mem_of_isLink`, `loopSet_subset_incidenceSet`, `mem_incidenceSet`, `mem_loopSet`, `mk_eq_self`	54
Total	65

Graph

Definitions

Name	Category	Theorems
`Inc` 📖	MathDef	8 math math: `IsLink.inc_left`, `isNonloopAt_iff_inc_not_isLoopAt`, `isLink_iff_inc`, `IsNonloopAt.inc`, `IsLoopAt.inc`, `IsLink.inc_right`, `mem_incidenceSet`, `isLoopAt_iff_inc_not_isNonloopAt`
`IsLink` 📖	MathDef	9 math math: `exists_isLink_of_mem_edgeSet`, `isLink_comm`, `isLink_iff_inc`, `ext_iff`, `Inc.isLink_other`, `edge_mem_iff_exists_isLink`, `edgeSet_eq_setOf_exists_isLink`, `isLink_symm`, `isLink_self_iff`
`IsLoopAt` 📖	MathDef	6 math math: `IsNonloopAt.not_isLoopAt`, `isNonloopAt_iff_inc_not_isLoopAt`, `mem_loopSet`, `Inc.isLoopAt_or_isNonloopAt`, `isLoopAt_iff_inc_not_isNonloopAt`, `isLink_self_iff`
`IsNonloopAt` 📖	MathDef	4 math math: `IsLoopAt.not_isNonloopAt`, `isNonloopAt_iff_inc_not_isLoopAt`, `Inc.isLoopAt_or_isNonloopAt`, `isLoopAt_iff_inc_not_isNonloopAt`
`edgeSet` 📖	CompOp	7 math math: `IsLink.edge_mem`, `IsNonloopAt.edge_mem`, `incidenceSet_subset_edgeSet`, `edge_mem_iff_exists_isLink`, `edgeSet_eq_setOf_exists_isLink`, `IsLoopAt.edge_mem`, `Inc.edge_mem`
`incidenceSet` 📖	CompOp	3 math math: `incidenceSet_subset_edgeSet`, `mem_incidenceSet`, `loopSet_subset_incidenceSet`
`loopSet` 📖	CompOp	2 math math: `mem_loopSet`, `loopSet_subset_incidenceSet`
`vertexSet` 📖	CompOp	10 math math: `Adj.right_mem`, `IsLink.right_mem`, `left_mem_of_isLink`, `IsLink.left_mem`, `IsNonloopAt.vertex_mem`, `ext_iff`, `Adj.left_mem`, `Inc.vertex_mem`, `IsLoopAt.vertex_mem`, `mk_eq_self`
`«termE(_)»` 📖» "API Documentation")	CompOp	—
`«termV(_)»` 📖» "API Documentation")	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adj_comm` 📖	mathematical	—	`Adj`	—	`Adj.symm`
`edgeSet_eq_setOf_exists_isLink` 📖	mathematical	—	`edgeSet` `setOf` `IsLink`	—	`Set.ext` `edge_mem_iff_exists_isLink`
`edge_mem_iff_exists_isLink` 📖	mathematical	—	`Set` `Set.instMembership` `edgeSet` `IsLink`	—	—
`eq_or_eq_of_isLink_of_isLink` 📖	—	`IsLink`	—	—	—
`exists_isLink_of_mem_edgeSet` 📖	mathematical	`Set` `Set.instMembership` `edgeSet`	`IsLink`	—	`edge_mem_iff_exists_isLink`
`ext` 📖	—	`vertexSet` `IsLink`	—	—	`edge_mem_iff_exists_isLink` `IsLink.left_eq_or_eq` `IsLink.left_mem` `mk_eq_self` `edgeSet_eq_setOf_exists_isLink`
`ext_iff` 📖	mathematical	—	`vertexSet` `IsLink`	—	`ext`
`ext_inc` 📖	—	`vertexSet` `Inc`	—	—	`ext`
`incidenceSet_subset_edgeSet` 📖	mathematical	—	`Set` `Set.instHasSubset` `incidenceSet` `edgeSet`	—	`IsLink.edge_mem`
`isLink_comm` 📖	mathematical	—	`IsLink`	—	`IsLink.symm`
`isLink_iff_inc` 📖	mathematical	—	`IsLink` `Inc`	—	`IsLink.inc_left` `IsLink.inc_right` `Inc.eq_or_eq_of_isLink` `IsLink.left_eq_or_eq` `IsLink.symm`
`isLink_self_iff` 📖	mathematical	—	`IsLink` `IsLoopAt`	—	—
`isLink_symm` 📖	mathematical	`Set` `Set.instMembership` `edgeSet`	`Symmetric` `IsLink`	—	—
`isLoopAt_iff_inc_not_isNonloopAt` 📖	mathematical	—	`IsLoopAt` `Inc` `IsNonloopAt`	—	—
`isNonloopAt_iff_inc_not_isLoopAt` 📖	mathematical	—	`IsNonloopAt` `Inc` `IsLoopAt`	—	`IsNonloopAt.inc` `IsNonloopAt.not_isLoopAt`
`left_mem_of_isLink` 📖	mathematical	`IsLink`	`Set` `Set.instMembership` `vertexSet`	—	—
`loopSet_subset_incidenceSet` 📖	mathematical	—	`Set` `Set.instHasSubset` `loopSet` `incidenceSet`	—	—
`mem_incidenceSet` 📖	mathematical	—	`Set` `Set.instMembership` `incidenceSet` `Inc`	—	—
`mem_loopSet` 📖	mathematical	—	`Set` `Set.instMembership` `loopSet` `IsLoopAt`	—	—
`mk_eq_self` 📖	mathematical	`Set` `Set.instMembership` `IsLink`	`vertexSet` `IsLink.left_eq_or_eq` `IsLink.left_mem`	—	`IsLink.left_eq_or_eq` `IsLink.left_mem` `edge_mem_iff_exists_isLink`

Graph.Adj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`left_mem` 📖	mathematical	`Graph.Adj`	`Set` `Set.instMembership` `Graph.vertexSet`	—	`Graph.IsLink.left_mem`
`right_mem` 📖	mathematical	`Graph.Adj`	`Set` `Set.instMembership` `Graph.vertexSet`	—	`left_mem` `symm`

Graph.Inc

Definitions

Name	Category	Theorems
`other` 📖	CompOp	2 math math: `inc_other`, `isLink_other`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`edge_mem` 📖	mathematical	`Graph.Inc`	`Set` `Set.instMembership` `Graph.edgeSet`	—	`Graph.IsLink.edge_mem`
`eq_of_isLink_of_ne_left` 📖	—	`Graph.Inc` `Graph.IsLink`	—	—	`eq_or_eq_of_isLink`
`eq_or_eq_of_isLink` 📖	—	`Graph.Inc` `Graph.IsLink`	—	—	`Graph.IsLink.left_eq_or_eq`
`eq_or_eq_or_eq` 📖	—	`Graph.Inc`	—	—	`eq_of_isLink_of_ne_left`
`inc_other` 📖	mathematical	`Graph.Inc`	`other`	—	`Graph.IsLink.inc_right` `isLink_other`
`isLink_other` 📖	mathematical	`Graph.Inc`	`Graph.IsLink` `other`	—	—
`isLoopAt_or_isNonloopAt` 📖	mathematical	`Graph.Inc`	`Graph.IsLoopAt` `Graph.IsNonloopAt`	—	—
`vertex_mem` 📖	mathematical	`Graph.Inc`	`Set` `Set.instMembership` `Graph.vertexSet`	—	`Graph.IsLink.left_mem`

Graph.IsLink

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adj` 📖	mathematical	`Graph.IsLink`	`Graph.Adj`	—	—
`edge_mem` 📖	mathematical	`Graph.IsLink`	`Set` `Set.instMembership` `Graph.edgeSet`	—	`Graph.edge_mem_iff_exists_isLink`
`eq_and_eq_or_eq_and_eq` 📖	—	`Graph.IsLink`	—	—	`left_eq_or_eq` `right_unique` `symm`
`inc_left` 📖	mathematical	`Graph.IsLink`	`Graph.Inc`	—	—
`inc_right` 📖	mathematical	`Graph.IsLink`	`Graph.Inc`	—	`symm`
`isLink_iff` 📖	—	`Graph.IsLink`	—	—	`eq_and_eq_or_eq_and_eq` `symm`
`isLink_iff_eq` 📖	—	`Graph.IsLink`	—	—	`right_unique`
`isLink_iff_sym2_eq` 📖	—	`Graph.IsLink`	—	—	`isLink_iff` `Sym2.eq_iff`
`left_eq_of_right_ne` 📖	—	`Graph.IsLink`	—	—	`left_eq_or_eq`
`left_eq_or_eq` 📖	—	`Graph.IsLink`	—	—	`Graph.eq_or_eq_of_isLink_of_isLink`
`left_mem` 📖	mathematical	`Graph.IsLink`	`Set` `Set.instMembership` `Graph.vertexSet`	—	`Graph.left_mem_of_isLink`
`left_unique` 📖	—	`Graph.IsLink`	—	—	`right_unique` `symm`
`right_eq_or_eq` 📖	—	`Graph.IsLink`	—	—	`left_eq_or_eq` `symm`
`right_mem` 📖	mathematical	`Graph.IsLink`	`Set` `Set.instMembership` `Graph.vertexSet`	—	`left_mem` `symm`
`right_unique` 📖	—	`Graph.IsLink`	—	—	`right_eq_or_eq` `symm`

Graph.IsLoopAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`edge_mem` 📖	mathematical	`Graph.IsLoopAt`	`Set` `Set.instMembership` `Graph.edgeSet`	—	`Graph.Inc.edge_mem` `inc`
`eq_of_inc` 📖	—	`Graph.IsLoopAt` `Graph.Inc`	—	—	`Graph.Inc.eq_or_eq_of_isLink`
`inc` 📖	mathematical	`Graph.IsLoopAt`	`Graph.Inc`	—	`Graph.IsLink.inc_left`
`not_isNonloopAt` 📖	mathematical	`Graph.IsLoopAt`	`Graph.IsNonloopAt`	—	`eq_of_inc` `Graph.IsLink.inc_right` `Graph.IsLink.inc_left`
`vertex_mem` 📖	mathematical	`Graph.IsLoopAt`	`Set` `Set.instMembership` `Graph.vertexSet`	—	`Graph.Inc.vertex_mem` `inc`

Graph.IsNonloopAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`edge_mem` 📖	mathematical	`Graph.IsNonloopAt`	`Set` `Set.instMembership` `Graph.edgeSet`	—	`Graph.Inc.edge_mem` `inc`
`inc` 📖	mathematical	`Graph.IsNonloopAt`	`Graph.Inc`	—	`Graph.IsLink.inc_left`
`not_isLoopAt` 📖	mathematical	`Graph.IsNonloopAt`	`Graph.IsLoopAt`	—	`Graph.IsLoopAt.not_isNonloopAt`
`vertex_mem` 📖	mathematical	`Graph.IsNonloopAt`	`Set` `Set.instMembership` `Graph.vertexSet`	—	`Graph.Inc.vertex_mem` `inc`

---

← Back to Index