Documentation Verification Report

Subgraph

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

Statistics

Metric	Count
Definitions `IsClosedSubgraph`, `IsInducedSubgraph`, `IsSpanningSubgraph`, `IsSubgraph`, `instPartialOrder`, `«term_≤c_»`, `«term_≤i_»`, `«term_≤s_»`	8
Theorems `mono`, `anti`, `anti_left`, `anti_right`, `ext`, `le_iff`, `of_ge`, `of_le`, `of_le_le`, `mono`, `adj_congr`, `anti_right`, `closed`, `inc_congr`, `instIsPartialOrder`, `isLink_congr`, `mem_iff_of_adj`, `mem_iff_of_isLink`, `mem_tfae_of_isLink`, `mk'`, `rfl`, `toIsInducedSubgraph`, `trans`, `adj_congr`, `anti_right`, `ext_of_vertexSet`, `instIsPartialOrder`, `isLink_congr`, `isLink_of_mem_mem`, `le`, `le_of_le_subset`, `not_isClosedSubgraph_iff_exists_adj`, `not_isClosedSubgraph_iff_exists_isLink`, `rfl`, `toIsSubgraph`, `trans`, `mono`, `mono`, `mono`, `anti_right`, `ext_of_edgeSet`, `instIsPartialOrder`, `le`, `mono_left`, `rfl`, `toIsSubgraph`, `trans`, `vertexSet_eq`, `antisymm`, `edgeSet_mono`, `inc_congr`, `inc_eqOn`, `isLink_eqOn`, `isLink_iff`, `isLink_mono`, `isLoopAt_congr`, `isLoopAt_eqOn`, `isNonloopAt_congr`, `isNonloopAt_eqOn`, `not_isInducedSubgraph_iff`, `trans`, `vertexSet_mono`, `isClosedSubgraph_iff`, `isInducedSubgraph_iff`, `isSpanningSubgraph_iff`, `isSubgraph_iff`, `isSubgraph_iff_le`, `le_iff_compatible_subset_subset`, `vertexSet_ssubset_or_edgeSet_ssubset_of_lt`	69
Total	77

Graph

Definitions

Name	Category	Theorems
`IsClosedSubgraph` 📖	CompData	8 math math: `IsClosedSubgraph.mk'`, `IsClosedSubgraph.trans`, `isClosedSubgraph_iff`, `IsClosedSubgraph.anti_right`, `IsClosedSubgraph.instIsPartialOrder`, `IsClosedSubgraph.rfl`, `IsInducedSubgraph.not_isClosedSubgraph_iff_exists_adj`, `IsInducedSubgraph.not_isClosedSubgraph_iff_exists_isLink`
`IsInducedSubgraph` 📖	CompData	8 math math: `IsClosedSubgraph.toIsInducedSubgraph`, `IsInducedSubgraph.anti_right`, `IsSubgraph.not_isInducedSubgraph_iff`, `isClosedSubgraph_iff`, `IsInducedSubgraph.instIsPartialOrder`, `IsInducedSubgraph.trans`, `isInducedSubgraph_iff`, `IsInducedSubgraph.rfl`
`IsSpanningSubgraph` 📖	CompData	6 math math: `IsSpanningSubgraph.anti_right`, `IsSpanningSubgraph.mono_left`, `IsSpanningSubgraph.rfl`, `IsSpanningSubgraph.instIsPartialOrder`, `IsSpanningSubgraph.trans`, `isSpanningSubgraph_iff`
`IsSubgraph` 📖	CompData	9 math math: `isSubgraph_iff`, `IsInducedSubgraph.le`, `IsSubgraph.trans`, `isInducedSubgraph_iff`, `IsSpanningSubgraph.toIsSubgraph`, `IsInducedSubgraph.toIsSubgraph`, `isSubgraph_iff_le`, `isSpanningSubgraph_iff`, `IsSpanningSubgraph.le`
`instPartialOrder` 📖	CompOp	4 math math: `IsInducedSubgraph.le_of_le_subset`, `Compatible.le_iff`, `isSubgraph_iff_le`, `le_iff_compatible_subset_subset`
`«term_≤c_»` 📖	CompOp	—
`«term_≤i_»` 📖	CompOp	—
`«term_≤s_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClosedSubgraph_iff` 📖	mathematical	—	`IsClosedSubgraph` `IsInducedSubgraph` `Set` `Set.instMembership` `edgeSet`	—	—
`isInducedSubgraph_iff` 📖	mathematical	—	`IsInducedSubgraph` `IsSubgraph` `IsLink`	—	—
`isSpanningSubgraph_iff` 📖	mathematical	—	`IsSpanningSubgraph` `IsSubgraph` `vertexSet`	—	—
`isSubgraph_iff` 📖	mathematical	—	`IsSubgraph` `Set` `Set.instHasSubset` `vertexSet`	—	—
`isSubgraph_iff_le` 📖	mathematical	—	`IsSubgraph` `Graph` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	—
`le_iff_compatible_subset_subset` 📖	mathematical	—	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Compatible` `Set` `Set.instHasSubset` `vertexSet` `edgeSet`	—	`Compatible.of_le` `IsSubgraph.vertexSet_mono` `IsSubgraph.edgeSet_mono` `IsLink.edge_mem`
`vertexSet_ssubset_or_edgeSet_ssubset_of_lt` 📖	mathematical	`Graph` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder`	`Set` `Set.instHasSSubset` `vertexSet` `edgeSet`	—	`Set.instIsNonstrictStrictOrderSubsetSSubset` `Set.instAntisymmSubset` `IsSubgraph.vertexSet_mono` `lt_iff_le_and_ne` `IsSubgraph.edgeSet_mono` `Compatible.ext` `Compatible.of_le_le` `le_rfl`

Graph.Adj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mono` 📖	mathematical	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `Graph.instPartialOrder` `Graph.Adj`	`Graph.Adj`	—	`Graph.IsLink.adj` `Graph.IsLink.mono`

Graph.Compatible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`anti` 📖	mathematical	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `Graph.instPartialOrder` `Graph.Compatible`	`Graph.Compatible`	—	`anti_right` `anti_left`
`anti_left` 📖	mathematical	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `Graph.instPartialOrder` `Graph.Compatible`	`Graph.Compatible`	—	`Graph.IsSubgraph.isLink_iff` `Graph.IsSubgraph.edgeSet_mono`
`anti_right` 📖	mathematical	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `Graph.instPartialOrder` `Graph.Compatible`	`Graph.Compatible`	—	`symm` `anti_left`
`ext` 📖	—	`Graph.vertexSet` `Graph.edgeSet` `Graph.Compatible`	—	—	`LE.le.antisymm` `le_iff` `Eq.subset` `Set.instReflSubset` `symm` `Eq.superset`
`le_iff` 📖	mathematical	`Graph.Compatible`	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `Graph.instPartialOrder` `Set` `Set.instHasSubset` `Graph.vertexSet` `Graph.edgeSet`	—	`Graph.le_iff_compatible_subset_subset`
`of_ge` 📖	mathematical	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `Graph.instPartialOrder`	`Graph.Compatible`	—	`of_le_le` `le_rfl`
`of_le` 📖	mathematical	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `Graph.instPartialOrder`	`Graph.Compatible`	—	`of_le_le` `le_rfl`
`of_le_le` 📖	mathematical	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `Graph.instPartialOrder`	`Graph.Compatible`	—	`Graph.IsSubgraph.isLink_iff`

Graph.Inc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mono` 📖	mathematical	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `Graph.instPartialOrder` `Graph.Inc`	`Graph.Inc`	—	`Graph.IsLink.inc_left` `Graph.IsLink.mono`

Graph.IsClosedSubgraph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adj_congr` 📖	mathematical	`Set` `Set.instMembership` `Graph.vertexSet` `Graph.IsClosedSubgraph`	`Graph.Adj`	—	`Graph.Adj.mono` `Graph.IsInducedSubgraph.le` `toIsInducedSubgraph` `Graph.IsLink.adj` `isLink_congr`
`anti_right` 📖	mathematical	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `Graph.instPartialOrder` `Graph.IsClosedSubgraph`	`Graph.IsClosedSubgraph`	—	`mk'` `Graph.Inc.edge_mem` `inc_congr` `Graph.Inc.mono`
`closed` 📖	mathematical	`Graph.IsClosedSubgraph` `Graph.Inc` `Set` `Set.instMembership` `Graph.vertexSet`	`Set` `Set.instMembership` `Graph.edgeSet`	—	—
`inc_congr` 📖	mathematical	`Set` `Set.instMembership` `Graph.vertexSet` `Graph.IsClosedSubgraph`	`Graph.Inc`	—	`Graph.Inc.mono` `Graph.IsInducedSubgraph.le` `toIsInducedSubgraph` `Graph.Inc.of_compatible` `Graph.Compatible.of_ge` `closed`
`instIsPartialOrder` 📖	mathematical	—	`IsPartialOrder` `Graph` `Graph.IsClosedSubgraph`	—	`mk'` `le_rfl` `Graph.Inc.edge_mem` `trans` `Graph.IsSubgraph.antisymm` `Graph.IsInducedSubgraph.le` `toIsInducedSubgraph`
`isLink_congr` 📖	mathematical	`Set` `Set.instMembership` `Graph.vertexSet` `Graph.IsClosedSubgraph`	`Graph.IsLink`	—	`Graph.IsLink.mono` `Graph.IsInducedSubgraph.le` `toIsInducedSubgraph` `Graph.Inc.edge_mem` `inc_congr` `Graph.IsLink.inc_left`
`mem_iff_of_adj` 📖	mathematical	`Graph.Adj` `Graph.IsClosedSubgraph`	`Set` `Set.instMembership` `Graph.vertexSet`	—	`mem_iff_of_isLink`
`mem_iff_of_isLink` 📖	mathematical	`Graph.IsLink` `Graph.IsClosedSubgraph`	`Set` `Set.instMembership` `Graph.vertexSet`	—	`Graph.IsLink.right_mem` `isLink_congr` `Graph.isLink_comm`
`mem_tfae_of_isLink` 📖	mathematical	`Graph.IsLink` `Graph.IsClosedSubgraph`	`List.TFAE` `Set` `Set.instMembership` `Graph.vertexSet` `Graph.edgeSet`	—	`mem_iff_of_isLink` `Graph.IsLink.edge_mem` `isLink_congr` `Graph.IsLink.symm` `Graph.IsLink.left_mem` `Graph.IsInducedSubgraph.le` `toIsInducedSubgraph` `List.tfae_of_cycle`
`mk'` 📖	mathematical	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `Graph.instPartialOrder` `Set` `Set.instMembership` `Graph.edgeSet`	`Graph.IsClosedSubgraph`	—	`Graph.IsLink.inc_left`
`rfl` 📖	mathematical	—	`Graph.IsClosedSubgraph`	—	`refl` `IsPreorder.toRefl` `IsPartialOrder.toIsPreorder` `instIsPartialOrder`
`toIsInducedSubgraph` 📖	mathematical	`Graph.IsClosedSubgraph`	`Graph.IsInducedSubgraph`	—	—
`trans` 📖	mathematical	`Graph.IsClosedSubgraph`	`Graph.IsClosedSubgraph`	—	`mk'` `Graph.IsSubgraph.trans` `Graph.IsInducedSubgraph.le` `toIsInducedSubgraph` `closed` `Graph.Inc.of_compatible` `Graph.Compatible.of_ge` `Graph.IsSubgraph.vertexSet_mono` `Graph.IsInducedSubgraph.toIsSubgraph`

Graph.IsInducedSubgraph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adj_congr` 📖	mathematical	`Set` `Set.instMembership` `Graph.vertexSet` `Graph.IsInducedSubgraph`	`Graph.Adj`	—	`Graph.Adj.mono` `le` `Graph.IsLink.adj` `isLink_of_mem_mem`
`anti_right` 📖	mathematical	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `Graph.instPartialOrder` `Graph.IsInducedSubgraph`	`Graph.IsInducedSubgraph`	—	`isLink_of_mem_mem` `Graph.IsLink.mono`
`ext_of_vertexSet` 📖	—	`Graph.vertexSet` `Graph.IsInducedSubgraph`	—	—	`Graph.Compatible.ext` `antisymm` `Set.instAntisymmSubset` `Graph.IsSubgraph.edgeSet_mono` `toIsSubgraph` `Graph.exists_isLink_of_mem_edgeSet` `Graph.IsLink.edge_mem` `isLink_of_mem_mem` `Graph.IsLink.left_mem` `Graph.IsLink.right_mem` `Graph.Compatible.of_le` `le`
`instIsPartialOrder` 📖	mathematical	—	`IsPartialOrder` `Graph` `Graph.IsInducedSubgraph`	—	`le_refl` `trans` `Graph.IsSubgraph.antisymm` `toIsSubgraph`
`isLink_congr` 📖	mathematical	`Set` `Set.instMembership` `Graph.vertexSet` `Graph.IsInducedSubgraph`	`Graph.IsLink`	—	`Graph.IsLink.mono` `le` `isLink_of_mem_mem`
`isLink_of_mem_mem` 📖	mathematical	`Graph.IsInducedSubgraph` `Graph.IsLink` `Set` `Set.instMembership` `Graph.vertexSet`	`Graph.IsLink`	—	—
`le` 📖	mathematical	`Graph.IsInducedSubgraph`	`Graph.IsSubgraph`	—	`toIsSubgraph`
`le_of_le_subset` 📖	mathematical	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `Graph.instPartialOrder` `Set` `Set.instHasSubset` `Graph.vertexSet` `Graph.IsInducedSubgraph`	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `Graph.instPartialOrder`	—	`Graph.Compatible.le_iff` `Graph.Compatible.of_le_le` `le` `Graph.exists_isLink_of_mem_edgeSet` `Graph.IsLink.edge_mem` `isLink_of_mem_mem` `Graph.IsLink.mono` `Graph.IsLink.left_mem` `Graph.IsLink.right_mem`
`not_isClosedSubgraph_iff_exists_adj` 📖	mathematical	`Graph.IsInducedSubgraph`	`Graph.IsClosedSubgraph` `Graph.Adj` `Set` `Set.instMembership` `Graph.vertexSet`	—	`Mathlib.Tactic.Contrapose.contrapose_iff₂` `Mathlib.Tactic.Push.not_and_eq` `Graph.IsLink.edge_mem` `isLink_of_mem_mem` `Graph.IsClosedSubgraph.mem_iff_of_adj`
`not_isClosedSubgraph_iff_exists_isLink` 📖	mathematical	`Graph.IsInducedSubgraph`	`Graph.IsClosedSubgraph` `Graph.IsLink` `Set` `Set.instMembership` `Graph.vertexSet`	—	`not_isClosedSubgraph_iff_exists_adj`
`rfl` 📖	mathematical	—	`Graph.IsInducedSubgraph`	—	`refl` `IsPreorder.toRefl` `IsPartialOrder.toIsPreorder` `instIsPartialOrder`
`toIsSubgraph` 📖	mathematical	`Graph.IsInducedSubgraph`	`Graph.IsSubgraph`	—	—
`trans` 📖	mathematical	`Graph.IsInducedSubgraph`	`Graph.IsInducedSubgraph`	—	`Graph.IsSubgraph.trans` `le` `isLink_of_mem_mem` `Graph.IsSubgraph.vertexSet_mono` `toIsSubgraph`

Graph.IsLink

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mono` 📖	mathematical	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `Graph.instPartialOrder` `Graph.IsLink`	`Graph.IsLink`	—	`Graph.IsSubgraph.isLink_mono`

Graph.IsLoopAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mono` 📖	mathematical	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `Graph.instPartialOrder` `Graph.IsLoopAt`	`Graph.IsLoopAt`	—	`Graph.IsLink.mono`

Graph.IsNonloopAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mono` 📖	mathematical	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `Graph.instPartialOrder` `Graph.IsNonloopAt`	`Graph.IsNonloopAt`	—	`Graph.IsLink.mono`

Graph.IsSpanningSubgraph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`anti_right` 📖	mathematical	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `Graph.instPartialOrder` `Graph.IsSpanningSubgraph`	`Graph.IsSpanningSubgraph`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `Graph.IsSubgraph.vertexSet_mono` `LE.le.trans_eq` `vertexSet_eq`
`ext_of_edgeSet` 📖	—	`Graph.edgeSet` `Graph.IsSpanningSubgraph`	—	—	`Graph.Compatible.ext` `vertexSet_eq` `Graph.Compatible.of_le` `le`
`instIsPartialOrder` 📖	mathematical	—	`IsPartialOrder` `Graph` `Graph.IsSpanningSubgraph`	—	`le_refl` `trans` `Graph.IsSubgraph.antisymm` `toIsSubgraph`
`le` 📖	mathematical	`Graph.IsSpanningSubgraph`	`Graph.IsSubgraph`	—	`toIsSubgraph`
`mono_left` 📖	mathematical	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `Graph.instPartialOrder` `Graph.IsSpanningSubgraph`	`Graph.IsSpanningSubgraph`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `Graph.IsSubgraph.vertexSet_mono` `LE.le.trans` `Eq.le` `vertexSet_eq`
`rfl` 📖	mathematical	—	`Graph.IsSpanningSubgraph`	—	`refl` `IsPreorder.toRefl` `IsPartialOrder.toIsPreorder` `instIsPartialOrder`
`toIsSubgraph` 📖	mathematical	`Graph.IsSpanningSubgraph`	`Graph.IsSubgraph`	—	—
`trans` 📖	mathematical	`Graph.IsSpanningSubgraph`	`Graph.IsSpanningSubgraph`	—	`Graph.IsSubgraph.trans` `le` `vertexSet_eq`
`vertexSet_eq` 📖	mathematical	`Graph.IsSpanningSubgraph`	`Graph.vertexSet`	—	—

Graph.IsSubgraph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antisymm` 📖	—	`Graph.IsSubgraph`	—	—	`Graph.ext` `HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `vertexSet_mono` `isLink_mono`
`edgeSet_mono` 📖	mathematical	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `Graph.instPartialOrder`	`Set` `Set.instHasSubset` `Graph.edgeSet`	—	`Graph.exists_isLink_of_mem_edgeSet` `Graph.IsLink.edge_mem` `Graph.IsLink.mono`
`inc_congr` 📖	mathematical	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `Graph.instPartialOrder` `Set` `Set.instMembership` `Graph.edgeSet`	`Graph.Inc`	—	`isLink_iff`
`inc_eqOn` 📖	mathematical	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `Graph.instPartialOrder`	`Set.EqOn` `Graph.Inc` `Graph.edgeSet`	—	`inc_congr`
`isLink_eqOn` 📖	mathematical	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `Graph.instPartialOrder`	`Set.EqOn` `Graph.IsLink` `Graph.edgeSet`	—	`isLink_iff`
`isLink_iff` 📖	mathematical	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `Graph.instPartialOrder` `Set` `Set.instMembership` `Graph.edgeSet`	`Graph.IsLink`	—	`Graph.IsLink.mono`
`isLink_mono` 📖	mathematical	`Graph.IsSubgraph` `Graph.IsLink`	`Graph.IsLink`	—	—
`isLoopAt_congr` 📖	mathematical	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `Graph.instPartialOrder` `Set` `Set.instMembership` `Graph.edgeSet`	`Graph.IsLoopAt`	—	`isLink_iff`
`isLoopAt_eqOn` 📖	mathematical	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `Graph.instPartialOrder`	`Set.EqOn` `Graph.IsLoopAt` `Graph.edgeSet`	—	`isLoopAt_congr`
`isNonloopAt_congr` 📖	mathematical	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `Graph.instPartialOrder` `Set` `Set.instMembership` `Graph.edgeSet`	`Graph.IsNonloopAt`	—	`isLink_iff`
`isNonloopAt_eqOn` 📖	mathematical	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `Graph.instPartialOrder`	`Set.EqOn` `Graph.IsNonloopAt` `Graph.edgeSet`	—	`isNonloopAt_congr`
`not_isInducedSubgraph_iff` 📖	mathematical	`Graph` `Preorder.toLE` `PartialOrder.toPreorder` `Graph.instPartialOrder`	`Graph.IsInducedSubgraph` `Graph.IsLink` `Set` `Set.instMembership` `Graph.vertexSet` `Graph.edgeSet`	—	`Mathlib.Tactic.Contrapose.contrapose_iff₂` `Mathlib.Tactic.Push.not_and_eq` `Graph.IsLink.edge_mem` `Graph.IsInducedSubgraph.isLink_of_mem_mem`
`trans` 📖	mathematical	`Graph.IsSubgraph`	`Graph.IsSubgraph`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `vertexSet_mono` `isLink_mono`
`vertexSet_mono` 📖	mathematical	`Graph.IsSubgraph`	`Set` `Set.instHasSubset` `Graph.vertexSet`	—	—

---

← Back to Index