Operations

📁 Source: Mathlib/Combinatorics/SimpleGraph/Operations.lean

Statistics

Metric	Count
Definitions `edge`, `instDecidableRelAdjEdge`, `instDecidableRelAdjReplaceVertex`, `instFintypeElemSym2EdgeSetEdge`, `replaceVertex`	5
Theorems `spanningCoe_sup_edge_le`, `adj_edge`, `adj_replaceVertex_iff_of_ne`, `adj_replaceVertex_iff_of_ne_left`, `adj_replaceVertex_iff_of_ne_right`, `card_edgeFinset_replaceVertex_of_adj`, `card_edgeFinset_replaceVertex_of_not_adj`, `card_edgeFinset_sup_edge`, `disjoint_edge`, `disjoint_sdiff_neighborFinset_image`, `edgeFinset_replaceVertex_of_adj`, `edgeFinset_replaceVertex_of_not_adj`, `edgeFinset_sup_edge`, `edgeSet_replaceVertex_of_adj`, `edgeSet_replaceVertex_of_not_adj`, `edge_adj`, `edge_comm`, `edge_edgeSet_of_ne`, `edge_le_iff`, `edge_self_eq_bot`, `lt_sup_edge`, `not_adj_replaceVertex_same`, `replaceVertex_self`, `sdiff_edge`, `sup_edge_of_adj`, `sup_edge_self`	26
Total	31

SimpleGraph

Definitions

Name	Category	Theorems
`edge` 📖	CompOp	21 math math: `card_edgeFinset_sup_edge`, `sup_edge_self`, `CliqueFree.sup_edge`, `lt_sup_edge`, `edge_edgeSet_of_ne`, `disjoint_edge`, `edge_self_eq_bot`, `edge_comm`, `Reachable.sum_sup_edge`, `adj_edge`, `isClique_sup_edge_of_ne_sdiff`, `edge_adj`, `Walk.IsPath.isCycles_spanningCoe_toSubgraph_sup_edge`, `sdiff_edge`, `Preconnected.sum_sup_edge`, `isClique_sup_edge_of_ne_iff`, `sup_edge_of_adj`, `edgeFinset_sup_edge`, `IsAlternating.sup_edge`, `edge_le_iff`, `Connected.sum_sup_edge`
`instDecidableRelAdjEdge` 📖	CompOp	—
`instDecidableRelAdjReplaceVertex` 📖	CompOp	4 math math: `edgeFinset_replaceVertex_of_adj`, `edgeFinset_replaceVertex_of_not_adj`, `card_edgeFinset_replaceVertex_of_not_adj`, `card_edgeFinset_replaceVertex_of_adj`
`instFintypeElemSym2EdgeSetEdge` 📖	CompOp	—
`replaceVertex` 📖	CompOp	12 math math: `adj_replaceVertex_iff_of_ne_right`, `adj_replaceVertex_iff_of_ne`, `CliqueFree.replaceVertex`, `adj_replaceVertex_iff_of_ne_left`, `edgeFinset_replaceVertex_of_adj`, `edgeSet_replaceVertex_of_adj`, `edgeFinset_replaceVertex_of_not_adj`, `replaceVertex_self`, `card_edgeFinset_replaceVertex_of_not_adj`, `card_edgeFinset_replaceVertex_of_adj`, `edgeSet_replaceVertex_of_not_adj`, `not_adj_replaceVertex_same`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adj_edge` 📖	mathematical	—	`Adj` `edge`	—	—
`adj_replaceVertex_iff_of_ne` 📖	mathematical	—	`Adj` `replaceVertex`	—	—
`adj_replaceVertex_iff_of_ne_left` 📖	mathematical	—	`Adj` `replaceVertex`	—	—
`adj_replaceVertex_iff_of_ne_right` 📖	mathematical	—	`Adj` `replaceVertex`	—	—
`card_edgeFinset_replaceVertex_of_adj` 📖	mathematical	`Adj`	`Finset.card` `Sym2` `edgeFinset` `replaceVertex` `fintypeEdgeSet` `Sym2.instFintype` `instDecidableRelAdjReplaceVertex` `degree` `neighborSetFintype`	—	`coe_edgeFinset` `edgeFinset_replaceVertex_of_adj` `Finset.card_sdiff_of_subset` `Finset.card_union_of_disjoint` `disjoint_sdiff_neighborFinset_image` `Finset.card_le_card` `card_incidenceFinset_eq_degree` `Finset.card_image_of_injective` `card_neighborFinset_eq_degree`
`card_edgeFinset_replaceVertex_of_not_adj` 📖	mathematical	`Adj`	`Finset.card` `Sym2` `edgeFinset` `replaceVertex` `fintypeEdgeSet` `Sym2.instFintype` `instDecidableRelAdjReplaceVertex` `degree` `neighborSetFintype`	—	`coe_edgeFinset` `edgeFinset_replaceVertex_of_not_adj` `Finset.card_union_of_disjoint` `disjoint_sdiff_neighborFinset_image` `Finset.card_sdiff_of_subset` `Finset.card_le_card` `card_incidenceFinset_eq_degree` `Finset.card_image_of_injective` `card_neighborFinset_eq_degree`
`card_edgeFinset_sup_edge` 📖	mathematical	`Adj`	`Finset.card` `Sym2` `edgeFinset` `SimpleGraph` `instMax` `edge` `fintypeEdgeSet` `Sym2.instFintype`	—	`edgeFinset_sup_edge` `Finset.card_cons`
`disjoint_edge` 📖	mathematical	—	`Disjoint` `SimpleGraph` `instPartialOrder` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `edge` `Adj`	—	`edge_self_eq_bot` `edge_edgeSet_of_ne`
`disjoint_sdiff_neighborFinset_image` 📖	mathematical	—	`Disjoint` `Finset` `Sym2` `Finset.partialOrder` `Finset.instOrderBot` `Finset.instSDiff` `Sym2.instDecidableEq` `edgeFinset` `fintypeEdgeSet` `Sym2.instFintype` `incidenceFinset` `neighborSetFintype` `Finset.image` `neighborFinset`	—	`Finset.disjoint_iff_ne` `mem_incidenceFinset` `Finset.mem_sdiff` `Mathlib.Tactic.Contrapose.contrapose₄`
`edgeFinset_replaceVertex_of_adj` 📖	mathematical	`Adj`	`edgeFinset` `replaceVertex` `fintypeEdgeSet` `Sym2.instFintype` `instDecidableRelAdjReplaceVertex` `Finset` `Sym2` `Finset.instSDiff` `Sym2.instDecidableEq` `Finset.instUnion` `incidenceFinset` `neighborSetFintype` `Finset.image` `neighborFinset` `Finset.instSingleton`	—	`Finset.coe_injective` `coe_edgeFinset` `Finset.coe_sdiff` `Finset.coe_union` `coe_incidenceFinset` `Finset.coe_image` `coe_neighborFinset` `Finset.coe_singleton` `edgeSet_replaceVertex_of_adj`
`edgeFinset_replaceVertex_of_not_adj` 📖	mathematical	`Adj`	`edgeFinset` `replaceVertex` `fintypeEdgeSet` `Sym2.instFintype` `instDecidableRelAdjReplaceVertex` `Finset` `Sym2` `Finset.instUnion` `Sym2.instDecidableEq` `Finset.instSDiff` `incidenceFinset` `neighborSetFintype` `Finset.image` `neighborFinset`	—	`Finset.coe_injective` `coe_edgeFinset` `Finset.coe_union` `Finset.coe_sdiff` `coe_incidenceFinset` `Finset.coe_image` `coe_neighborFinset` `edgeSet_replaceVertex_of_not_adj`
`edgeFinset_sup_edge` 📖	mathematical	`Adj`	`edgeFinset` `SimpleGraph` `instMax` `edge` `Finset.cons` `Sym2` `fintypeEdgeSet` `Sym2.instFintype`	—	`edgeFinset_sup` `Finset.cons_eq_insert` `Finset.insert_eq` `Finset.union_comm` `Set.toFinset_congr` `edge_edgeSet_of_ne`
`edgeSet_replaceVertex_of_adj` 📖	mathematical	`Adj`	`edgeSet` `replaceVertex` `Set` `Sym2` `Set.instSDiff` `Set.instUnion` `incidenceSet` `Set.image` `neighborSet` `Set.instSingletonSet`	—	`Set.ext` `Sym2.inductionOn` `adj_comm`
`edgeSet_replaceVertex_of_not_adj` 📖	mathematical	`Adj`	`edgeSet` `replaceVertex` `Set` `Sym2` `Set.instUnion` `Set.instSDiff` `incidenceSet` `Set.image` `neighborSet`	—	`Set.ext` `Sym2.inductionOn` `adj_comm`
`edge_adj` 📖	mathematical	—	`Adj` `edge`	—	`edge.eq_1` `fromEdgeSet_adj` `Set.mem_singleton_iff` `Sym2.eq_iff`
`edge_comm` 📖	mathematical	—	`edge`	—	`edge.eq_1` `Sym2.eq_swap`
`edge_edgeSet_of_ne` 📖	mathematical	—	`edgeSet` `edge` `Sym2` `Set` `Set.instSingletonSet`	—	`edgeSet_fromEdgeSet`
`edge_le_iff` 📖	mathematical	—	`SimpleGraph` `instLE` `edge` `Adj`	—	`eq_or_ne` `edge_self_eq_bot`
`edge_self_eq_bot` 📖	mathematical	—	`edge` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`ext` `edge_adj`
`lt_sup_edge` 📖	mathematical	`Adj`	`SimpleGraph` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `instMax` `edge`	—	`left_lt_sup` `edge_adj`
`not_adj_replaceVertex_same` 📖	mathematical	—	`Adj` `replaceVertex`	—	—
`replaceVertex_self` 📖	mathematical	—	`replaceVertex`	—	`ext`
`sdiff_edge` 📖	mathematical	`Adj`	`SimpleGraph` `sdiff` `edge`	—	—
`sup_edge_of_adj` 📖	mathematical	`Adj`	`SimpleGraph` `instMax` `edge`	—	`sup_eq_left` `edgeSet_subset_edgeSet` `edge_edgeSet_of_ne` `Adj.ne` `Set.singleton_subset_iff` `mem_edgeSet`
`sup_edge_self` 📖	mathematical	—	`SimpleGraph` `instMax` `edge`	—	`edge_self_eq_bot` `sup_of_le_left`

SimpleGraph.Subgraph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`spanningCoe_sup_edge_le` 📖	mathematical	`Adj` `SimpleGraph` `SimpleGraph.instMax` `SimpleGraph.edge`	`SimpleGraph.instLE` `spanningCoe`	—	`Adj.adj_sub` `adj_congr_of_sym2`

---

← Back to Index