Basic

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

Statistics

Metric	Count
Definitions `Compatible`, `Inc`, `other`, `IsLink`, `IsLoopAt`, `IsNonloopAt`, `banana`, `bouquet`, `copy`, `edgeSet`, `incidenceSet`, `loopSet`, `noEdge`, `vertexSet`, `«termE(_)»`»), `«termV(_)»`»)	16
Theorems `left_mem`, `right_mem`, `isLink_congr`, `of_disjoint_edgeSet`, `refl`, `rfl`, `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`, `of_compatible`, `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`, `of_compatible`, `right_eq_or_eq`, `right_mem`, `right_unique`, `edge_mem`, `eq_of_inc`, `inc`, `not_isNonloopAt`, `of_compatible`, `vertex_mem`, `edge_mem`, `inc`, `not_isLoopAt`, `of_compatible`, `vertex_mem`, `adj_comm`, `banana_adj`, `banana_comm`, `banana_edgeSet`, `banana_empty`, `banana_inc`, `banana_isLink`, `banana_isLoopAt`, `banana_isNonloopAt`, `banana_vertexSet`, `bouquet_adj`, `bouquet_empty`, `bouquet_inc`, `bouquet_isLink`, `bouquet_isLoopAt`, `bouquet_vertexSet`, `copy_edgeSet`, `copy_eq`, `copy_isLink`, `copy_vertexSet`, `edgeSet_eq_empty`, `edgeSet_eq_setOf_exists_isLink`, `edge_mem_iff_exists_isLink`, `eq_bouquet_iff`, `eq_bouquet_of_subsingleton`, `eq_or_eq_of_isLink_of_isLink`, `exists_eq_bouquet`, `exists_isLink_of_mem_edgeSet`, `ext`, `ext_iff`, `ext_inc`, `inc_eq_inc_iff_isLink_eq_isLink`, `incidenceSet_subset_edgeSet`, `instReflCompatible`, `instSymmAdj`, `instSymmCompatible`, `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`, `noEdge_edgeSet`, `noEdge_isLink`, `noEdge_vertexSet`, `not_inc_of_notMem_edgeSet`, `not_isLink_of_notMem_edgeSet`, `not_isNonloopAt_bouquet`	95
Total	111

Graph

Definitions

Name	Category	Theorems
`Compatible` 📖	MathDef	13 math math: `instReflCompatible`, `Compatible.refl`, `Compatible.of_le`, `Compatible.of_ge`, `Compatible.anti_right`, `instSymmCompatible`, `Compatible.of_disjoint_edgeSet`, `Compatible.anti_left`, `Compatible.symm`, `Compatible.rfl`, `Compatible.of_le_le`, `le_iff_compatible_subset_subset`, `Compatible.anti`
`Inc` 📖	MathDef	18 math math: `inc_eq_inc_iff_isLink_eq_isLink`, `IsLink.inc_left`, `Inc.of_compatible`, `banana_inc`, `Inc.inc_other`, `isNonloopAt_iff_inc_not_isLoopAt`, `isLink_iff_inc`, `IsClosedSubgraph.inc_congr`, `Inc.mono`, `IsNonloopAt.inc`, `IsSubgraph.inc_congr`, `IsLoopAt.inc`, `IsLink.inc_right`, `mem_incidenceSet`, `isLoopAt_iff_inc_not_isNonloopAt`, `IsSubgraph.inc_eqOn`, `not_inc_of_notMem_edgeSet`, `bouquet_inc`
`IsLink` 📖	MathDef	32 math math: `IsLink.isLink_iff`, `exists_isLink_of_mem_edgeSet`, `isLink_comm`, `IsLink.mono`, `inc_eq_inc_iff_isLink_eq_isLink`, `IsSubgraph.isLink_eqOn`, `IsSubgraph.isLink_iff`, `Compatible.isLink_congr`, `IsLink.isLink_iff_sym2_eq`, `IsClosedSubgraph.isLink_congr`, `banana_isLink`, `isLink_iff_inc`, `noEdge_isLink`, `IsLink.of_compatible`, `IsSubgraph.isLink_mono`, `ext_iff`, `IsSubgraph.not_isInducedSubgraph_iff`, `Inc.isLink_other`, `IsLink.symm`, `bouquet_isLink`, `copy_isLink`, `not_isLink_of_notMem_edgeSet`, `edge_mem_iff_exists_isLink`, `isInducedSubgraph_iff`, `edgeSet_eq_setOf_exists_isLink`, `isLink_symm`, `IsInducedSubgraph.isLink_of_mem_mem`, `isLink_self_iff`, `IsInducedSubgraph.isLink_congr`, `IsLink.isLink_iff_eq`, `mk_eq_self`, `IsInducedSubgraph.not_isClosedSubgraph_iff_exists_isLink`
`IsLoopAt` 📖	MathDef	12 math math: `IsNonloopAt.not_isLoopAt`, `isNonloopAt_iff_inc_not_isLoopAt`, `banana_isLoopAt`, `mem_loopSet`, `IsLoopAt.mono`, `Inc.isLoopAt_or_isNonloopAt`, `isLoopAt_iff_inc_not_isNonloopAt`, `IsSubgraph.isLoopAt_congr`, `isLink_self_iff`, `IsLoopAt.of_compatible`, `bouquet_isLoopAt`, `IsSubgraph.isLoopAt_eqOn`
`IsNonloopAt` 📖	MathDef	10 math math: `IsLoopAt.not_isNonloopAt`, `isNonloopAt_iff_inc_not_isLoopAt`, `not_isNonloopAt_bouquet`, `banana_isNonloopAt`, `IsNonloopAt.of_compatible`, `Inc.isLoopAt_or_isNonloopAt`, `isLoopAt_iff_inc_not_isNonloopAt`, `IsNonloopAt.mono`, `IsSubgraph.isNonloopAt_eqOn`, `IsSubgraph.isNonloopAt_congr`
`banana` 📖	CompOp	9 math math: `banana_inc`, `banana_isLink`, `banana_edgeSet`, `banana_comm`, `banana_isLoopAt`, `banana_isNonloopAt`, `banana_vertexSet`, `banana_adj`, `banana_empty`
`bouquet` 📖	CompOp	10 math math: `eq_bouquet_iff`, `not_isNonloopAt_bouquet`, `bouquet_empty`, `exists_eq_bouquet`, `bouquet_isLink`, `bouquet_vertexSet`, `eq_bouquet_of_subsingleton`, `bouquet_inc`, `bouquet_adj`, `bouquet_isLoopAt`
`copy` 📖	CompOp	4 math math: `copy_isLink`, `copy_eq`, `copy_edgeSet`, `copy_vertexSet`
`edgeSet` 📖	CompOp	25 math math: `IsLink.edge_mem`, `IsSubgraph.isLink_eqOn`, `IsClosedSubgraph.mem_tfae_of_isLink`, `IsNonloopAt.edge_mem`, `IsSubgraph.edgeSet_mono`, `banana_edgeSet`, `eq_bouquet_iff`, `IsSubgraph.not_isInducedSubgraph_iff`, `vertexSet_ssubset_or_edgeSet_ssubset_of_lt`, `IsClosedSubgraph.closed`, `isClosedSubgraph_iff`, `incidenceSet_subset_edgeSet`, `noEdge_edgeSet`, `Compatible.le_iff`, `edge_mem_iff_exists_isLink`, `edgeSet_eq_setOf_exists_isLink`, `edgeSet_eq_empty`, `eq_bouquet_of_subsingleton`, `IsSubgraph.inc_eqOn`, `IsLoopAt.edge_mem`, `IsSubgraph.isNonloopAt_eqOn`, `copy_edgeSet`, `le_iff_compatible_subset_subset`, `IsSubgraph.isLoopAt_eqOn`, `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`
`noEdge` 📖	CompOp	6 math math: `noEdge_vertexSet`, `noEdge_isLink`, `bouquet_empty`, `noEdge_edgeSet`, `edgeSet_eq_empty`, `banana_empty`
`vertexSet` 📖	CompOp	29 math math: `isSubgraph_iff`, `Adj.right_mem`, `noEdge_vertexSet`, `IsClosedSubgraph.mem_tfae_of_isLink`, `IsLink.right_mem`, `eq_bouquet_iff`, `left_mem_of_isLink`, `IsLink.left_mem`, `IsNonloopAt.vertex_mem`, `ext_iff`, `Adj.left_mem`, `IsSubgraph.not_isInducedSubgraph_iff`, `vertexSet_ssubset_or_edgeSet_ssubset_of_lt`, `IsClosedSubgraph.mem_iff_of_adj`, `Inc.vertex_mem`, `bouquet_vertexSet`, `banana_vertexSet`, `Compatible.le_iff`, `IsSpanningSubgraph.vertexSet_eq`, `IsInducedSubgraph.not_isClosedSubgraph_iff_exists_adj`, `edgeSet_eq_empty`, `isSpanningSubgraph_iff`, `copy_vertexSet`, `le_iff_compatible_subset_subset`, `IsLoopAt.vertex_mem`, `mk_eq_self`, `IsSubgraph.vertexSet_mono`, `IsClosedSubgraph.mem_iff_of_isLink`, `IsInducedSubgraph.not_isClosedSubgraph_iff_exists_isLink`
`«termE(_)»` 📖» "API Documentation")	CompOp	—
`«termV(_)»` 📖» "API Documentation")	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adj_comm` 📖	mathematical	—	`Adj`	—	`Adj.symm`
`banana_adj` 📖	mathematical	—	`Adj` `banana` `Set.Nonempty`	—	—
`banana_comm` 📖	mathematical	—	`banana`	—	`ext_inc` `Set.pair_comm`
`banana_edgeSet` 📖	mathematical	—	`edgeSet` `banana`	—	—
`banana_empty` 📖	mathematical	—	`banana` `Set` `Set.instEmptyCollection` `noEdge` `Set.instInsert` `Set.instSingletonSet`	—	`ext` `Set.ext`
`banana_inc` 📖	mathematical	—	`Inc` `banana` `Set` `Set.instMembership`	—	—
`banana_isLink` 📖	mathematical	—	`IsLink` `banana` `Set` `Set.instMembership`	—	—
`banana_isLoopAt` 📖	mathematical	—	`IsLoopAt` `banana` `Set` `Set.instMembership`	—	—
`banana_isNonloopAt` 📖	mathematical	—	`IsNonloopAt` `banana` `Set` `Set.instMembership`	—	—
`banana_vertexSet` 📖	mathematical	—	`vertexSet` `banana` `Set` `Set.instInsert` `Set.instSingletonSet`	—	—
`bouquet_adj` 📖	mathematical	—	`Adj` `bouquet` `Set.Nonempty`	—	—
`bouquet_empty` 📖	mathematical	—	`bouquet` `Set` `Set.instEmptyCollection` `noEdge` `Set.instSingletonSet`	—	`banana_empty` `Set.insert_eq_of_mem`
`bouquet_inc` 📖	mathematical	—	`Inc` `bouquet` `Set` `Set.instMembership`	—	—
`bouquet_isLink` 📖	mathematical	—	`IsLink` `bouquet` `Set` `Set.instMembership`	—	—
`bouquet_isLoopAt` 📖	mathematical	—	`IsLoopAt` `bouquet` `Set` `Set.instMembership`	—	—
`bouquet_vertexSet` 📖	mathematical	—	`vertexSet` `bouquet` `Set` `Set.instSingletonSet`	—	`Set.insert_eq_of_mem`
`copy_edgeSet` 📖	mathematical	`vertexSet` `edgeSet` `IsLink`	`edgeSet` `copy`	—	—
`copy_eq` 📖	mathematical	`vertexSet` `edgeSet` `IsLink`	`copy`	—	`ext` `Set.ext`
`copy_isLink` 📖	mathematical	`vertexSet` `edgeSet` `IsLink`	`IsLink` `copy`	—	—
`copy_vertexSet` 📖	mathematical	`vertexSet` `edgeSet` `IsLink`	`vertexSet` `copy`	—	—
`edgeSet_eq_empty` 📖	mathematical	—	`edgeSet` `Set` `Set.instEmptyCollection` `noEdge` `vertexSet`	—	`ext` `IsLink.edge_mem` `noEdge_edgeSet`
`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_bouquet_iff` 📖	mathematical	—	`bouquet` `edgeSet` `vertexSet` `Set` `Set.instSingletonSet`	—	`bouquet_vertexSet` `eq_bouquet_of_subsingleton`
`eq_bouquet_of_subsingleton` 📖	mathematical	`Set` `Set.instMembership` `vertexSet` `Set.Subsingleton`	`bouquet` `edgeSet`	—	`Set.Subsingleton.eq_singleton_of_mem` `ext_inc` `Set.insert_eq_of_mem` `Inc.edge_mem` `Inc.vertex_mem` `exists_isLink_of_mem_edgeSet` `IsLink.left_mem` `IsLink.inc_left`
`eq_or_eq_of_isLink_of_isLink` 📖	—	`IsLink`	—	—	—
`exists_eq_bouquet` 📖	mathematical	`Set.Nonempty` `vertexSet` `Set.Subsingleton`	`Set` `bouquet`	—	`eq_bouquet_of_subsingleton` `Set.Nonempty.some_mem`
`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`
`inc_eq_inc_iff_isLink_eq_isLink` 📖	mathematical	—	`Inc` `IsLink`	—	`isLink_iff_inc`
`incidenceSet_subset_edgeSet` 📖	mathematical	—	`Set` `Set.instHasSubset` `incidenceSet` `edgeSet`	—	`IsLink.edge_mem`
`instReflCompatible` 📖	mathematical	—	`Graph` `Compatible`	—	`Compatible.rfl`
`instSymmAdj` 📖	mathematical	—	`Adj`	—	`Adj.symm`
`instSymmCompatible` 📖	mathematical	—	`Graph` `Compatible`	—	`Compatible.symm`
`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` `IsLink.left_eq_or_eq` `IsLink.left_mem`	—	`IsLink.left_eq_or_eq` `IsLink.left_mem` `edge_mem_iff_exists_isLink`
`noEdge_edgeSet` 📖	mathematical	—	`edgeSet` `noEdge` `Set` `Set.instEmptyCollection`	—	—
`noEdge_isLink` 📖	mathematical	—	`IsLink` `noEdge`	—	—
`noEdge_vertexSet` 📖	mathematical	—	`vertexSet` `noEdge`	—	—
`not_inc_of_notMem_edgeSet` 📖	mathematical	`Set` `Set.instMembership` `edgeSet`	`Inc`	—	`Inc.edge_mem`
`not_isLink_of_notMem_edgeSet` 📖	mathematical	`Set` `Set.instMembership` `edgeSet`	`IsLink`	—	`IsLink.edge_mem`
`not_isNonloopAt_bouquet` 📖	mathematical	—	`IsNonloopAt` `bouquet`	—	—

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.Compatible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLink_congr` 📖	mathematical	`Set` `Set.instMembership` `Graph.edgeSet` `Graph.Compatible`	`Graph.IsLink`	—	—
`of_disjoint_edgeSet` 📖	mathematical	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `Set.instBooleanAlgebra` `HeytingAlgebra.toOrderBot` `BiheytingAlgebra.toHeytingAlgebra` `Graph.edgeSet`	`Graph.Compatible`	—	`Disjoint.notMem_of_mem_left`
`refl` 📖	mathematical	—	`Graph.Compatible`	—	—
`rfl` 📖	mathematical	—	`Graph.Compatible`	—	`refl`

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`	`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`	—	—
`of_compatible` 📖	mathematical	`Graph.Compatible` `Set` `Set.instMembership` `Graph.edgeSet` `Graph.Inc`	`Graph.Inc`	—	`Graph.IsLink.of_compatible`
`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` 📖	mathematical	`Graph.IsLink`	`Graph.IsLink`	—	`eq_and_eq_or_eq_and_eq` `symm`
`isLink_iff_eq` 📖	mathematical	`Graph.IsLink`	`Graph.IsLink`	—	`right_unique`
`isLink_iff_sym2_eq` 📖	mathematical	`Graph.IsLink`	`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`
`of_compatible` 📖	mathematical	`Graph.Compatible` `Set` `Set.instMembership` `Graph.edgeSet` `Graph.IsLink`	`Graph.IsLink`	—	`edge_mem`
`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`
`of_compatible` 📖	mathematical	`Graph.Compatible` `Set` `Set.instMembership` `Graph.edgeSet` `Graph.IsLoopAt`	`Graph.IsLoopAt`	—	`Graph.IsLink.of_compatible`
`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`
`of_compatible` 📖	mathematical	`Graph.Compatible` `Set` `Set.instMembership` `Graph.edgeSet` `Graph.IsNonloopAt`	`Graph.IsNonloopAt`	—	`Graph.IsLink.of_compatible`
`vertex_mem` 📖	mathematical	`Graph.IsNonloopAt`	`Set` `Set.instMembership` `Graph.vertexSet`	—	`Graph.Inc.vertex_mem` `inc`

---

← Back to Index