DeleteEdges

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

Statistics

Metric	Count
Definitions `DeleteFar`, `deleteEdges`, `deleteIncidenceSet`, `instDecidableRelAdjDeleteEdgesOfDecidablePredSym2MemSetOfDecidableEq`, `instDecidableRelAdjDeleteIncidenceSet`	5
Theorems `le_card_edgeFinset`, `le_card_sub_card`, `mono`, `card_edgeFinset_deleteIncidenceSet`, `card_edgeFinset_induce_compl_singleton`, `card_support_deleteIncidenceSet`, `deleteEdges_adj`, `deleteEdges_anti`, `deleteEdges_deleteEdges`, `deleteEdges_edgeSet`, `deleteEdges_empty`, `deleteEdges_eq_inter_edgeSet`, `deleteEdges_eq_self`, `deleteEdges_fromEdgeSet`, `deleteEdges_le`, `deleteEdges_mono`, `deleteEdges_of_subset_diagSet`, `deleteEdges_sdiff_eq_of_le`, `deleteEdges_sup`, `deleteEdges_univ`, `deleteFar_iff`, `deleteIncidenceSet_adj`, `deleteIncidenceSet_le`, `edgeFinset_deleteEdges`, `edgeFinset_deleteIncidenceSet_eq_filter`, `edgeFinset_deleteIncidenceSet_eq_sdiff`, `edgeSet_deleteEdges`, `edgeSet_deleteIncidenceSet`, `edgeSet_fromEdgeSet_incidenceSet`, `induce_deleteIncidenceSet_of_notMem`, `support_deleteIncidenceSet_subset`	31
Total	36

SimpleGraph

Definitions

Name	Category	Theorems
`DeleteFar` 📖	MathDef	1 math math: `deleteFar_iff`
`deleteEdges` 📖	CompOp	32 math math: `Connected.connected_delete_edge_of_not_isBridge`, `isEdgeConnected_two`, `deleteEdges_edgeSet`, `isEdgeReachable_add_one`, `Subgraph.deleteEdges_spanningCoe_eq`, `Walk.map_toDeleteEdges_eq`, `deleteEdges_fromEdgeSet`, `deleteEdges_univ`, `isEdgeConnected_add_one`, `Walk.IsCycle.toDeleteEdges`, `Walk.toDeleteEdges_copy`, `isEdgeReachable_two`, `Subgraph.deleteEdges_coe_eq`, `deleteEdges_anti`, `deleteEdges_adj`, `deleteEdges_sup`, `deleteEdges_empty`, `deleteEdges_eq_inter_edgeSet`, `IsCycles.reachable_deleteEdges`, `Walk.IsPath.toDeleteEdges`, `Walk.toDeleteEdges_cons`, `edgeSet_deleteEdges`, `Walk.toDeleteEdges_nil`, `killCopies_def`, `deleteEdges_of_subset_diagSet`, `edgeFinset_deleteEdges`, `deleteEdges_sdiff_eq_of_le`, `deleteEdges_eq_self`, `deleteEdges_deleteEdges`, `deleteEdges_mono`, `Subgraph.coe_deleteEdges_eq`, `deleteEdges_le`
`deleteIncidenceSet` 📖	CompOp	11 math math: `deleteIncidenceSet_le`, `edgeFinset_deleteIncidenceSet_eq_sdiff`, `deleteIncidenceSet_adj`, `induce_deleteIncidenceSet_of_notMem`, `edgeSet_deleteIncidenceSet`, `card_edgeFinset_deleteIncidenceSet_le_extremalNumber`, `edgeFinset_deleteIncidenceSet_eq_filter`, `card_support_deleteIncidenceSet`, `card_edgeFinset_deleteIncidenceSet`, `support_deleteIncidenceSet_subset`, `card_edgeFinset_induce_compl_singleton`
`instDecidableRelAdjDeleteEdgesOfDecidablePredSym2MemSetOfDecidableEq` 📖	CompOp	—
`instDecidableRelAdjDeleteIncidenceSet` 📖	CompOp	6 math math: `edgeFinset_deleteIncidenceSet_eq_sdiff`, `card_edgeFinset_deleteIncidenceSet_le_extremalNumber`, `edgeFinset_deleteIncidenceSet_eq_filter`, `card_support_deleteIncidenceSet`, `card_edgeFinset_deleteIncidenceSet`, `card_edgeFinset_induce_compl_singleton`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_edgeFinset_deleteIncidenceSet` 📖	mathematical	—	`Finset.card` `Sym2` `edgeFinset` `deleteIncidenceSet` `fintypeEdgeSet` `Sym2.instFintype` `instDecidableRelAdjDeleteIncidenceSet` `degree` `neighborSetFintype`	—	`Finset.card_sdiff_of_subset` `incidenceFinset_subset` `edgeFinset_deleteIncidenceSet_eq_sdiff`
`card_edgeFinset_induce_compl_singleton` 📖	mathematical	—	`Finset.card` `Sym2` `Set.Elem` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `edgeFinset` `induce` `fintypeEdgeSet` `Sym2.instFintype` `Subtype.fintype` `Set.instMembership` `Set.decidableCompl` `Set.decidableSingleton` `instDecidableComapAdj` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `Function.Embedding.subtype` `deleteIncidenceSet` `instDecidableRelAdjDeleteIncidenceSet`	—	`Set.notMem_compl_iff` `Set.mem_singleton` `Set.toFinset_card` `Fintype.card_congr'` `induce_deleteIncidenceSet_of_notMem` `card_edgeFinset_induce_of_support_subset` `support_deleteIncidenceSet_subset` `Set.compl_eq_univ_diff` `Set.diff_subset_diff_left` `Set.subset_univ`
`card_support_deleteIncidenceSet` 📖	mathematical	`Set` `Set.instMembership` `support`	`Fintype.card` `Set.Elem` `deleteIncidenceSet` `Subtype.fintype` `instDecidablePredMemSetSupport` `instDecidableRelAdjDeleteIncidenceSet`	—	`Finset.card_sdiff_of_subset` `Set.toFinset_subset_toFinset` `Set.singleton_subset_iff` `Finset.card_le_card` `support_deleteIncidenceSet_subset`
`deleteEdges_adj` 📖	mathematical	—	`Adj` `deleteEdges` `Sym2` `Set` `Set.instMembership`	—	`Iff.not` `Adj.ne`
`deleteEdges_anti` 📖	mathematical	`Set` `Sym2` `Set.instHasSubset`	`SimpleGraph` `instLE` `deleteEdges`	—	`sdiff_le_sdiff_left` `fromEdgeSet_mono`
`deleteEdges_deleteEdges` 📖	mathematical	—	`deleteEdges` `Set` `Sym2` `Set.instUnion`	—	`sdiff_sdiff` `fromEdgeSet_union`
`deleteEdges_edgeSet` 📖	mathematical	—	`deleteEdges` `edgeSet` `SimpleGraph` `sdiff`	—	`ext`
`deleteEdges_empty` 📖	mathematical	—	`deleteEdges` `Set` `Sym2` `Set.instEmptyCollection`	—	`fromEdgeSet_empty` `sdiff_bot`
`deleteEdges_eq_inter_edgeSet` 📖	mathematical	—	`deleteEdges` `Set` `Sym2` `Set.instInter` `edgeSet`	—	`ext`
`deleteEdges_eq_self` 📖	mathematical	—	`deleteEdges` `Disjoint` `Set` `Sym2` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `edgeSet`	—	`deleteEdges.eq_1` `sdiff_eq_left` `disjoint_fromEdgeSet`
`deleteEdges_fromEdgeSet` 📖	mathematical	—	`deleteEdges` `fromEdgeSet` `Set` `Sym2` `Set.instSDiff`	—	`ext` `fromEdgeSet_sdiff`
`deleteEdges_le` 📖	mathematical	—	`SimpleGraph` `instLE` `deleteEdges`	—	`sdiff_le`
`deleteEdges_mono` 📖	mathematical	`SimpleGraph` `instLE`	`deleteEdges`	—	`sdiff_le_sdiff_right`
`deleteEdges_of_subset_diagSet` 📖	mathematical	`Set` `Sym2` `Set.instHasSubset` `Sym2.diagSet`	`deleteEdges`	—	`ext` `Adj.ne`
`deleteEdges_sdiff_eq_of_le` 📖	mathematical	`SimpleGraph` `instLE`	`deleteEdges` `Set` `Sym2` `Set.instSDiff` `edgeSet`	—	`edgeSet_sdiff` `deleteEdges_edgeSet` `sdiff_sdiff_eq_self`
`deleteEdges_sup` 📖	mathematical	—	`deleteEdges` `SimpleGraph` `instMax`	—	`sup_sdiff`
`deleteEdges_univ` 📖	mathematical	—	`deleteEdges` `Set.univ` `Sym2` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`fromEdgeSet_univ` `sdiff_top`
`deleteFar_iff` 📖	mathematical	—	`DeleteFar` `Preorder.toLE` `PartialOrder.toPreorder` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Finset.card` `Sym2` `edgeFinset` `fintypeEdgeSet`	—	`Finset.sdiff_subset` `Finset.coe_sdiff` `coe_edgeFinset` `deleteEdges_sdiff_eq_of_le` `Finset.card_sdiff_of_subset` `edgeFinset_mono` `Nat.cast_sub` `edgeFinset_deleteEdges` `Finset.card_le_card` `sub_sub_cancel` `deleteEdges_le`
`deleteIncidenceSet_adj` 📖	mathematical	—	`Adj` `deleteIncidenceSet`	—	`deleteIncidenceSet.eq_1` `deleteEdges_adj` `mk'_mem_incidenceSet_iff`
`deleteIncidenceSet_le` 📖	mathematical	—	`SimpleGraph` `instLE` `deleteIncidenceSet`	—	`deleteEdges_le`
`edgeFinset_deleteEdges` 📖	mathematical	—	`edgeFinset` `deleteEdges` `SetLike.coe` `Finset` `Sym2` `Finset.instSetLike` `Finset.instSDiff` `Sym2.instDecidableEq`	—	`Finset.ext` `edgeSet_deleteEdges`
`edgeFinset_deleteIncidenceSet_eq_filter` 📖	mathematical	—	`edgeFinset` `deleteIncidenceSet` `fintypeEdgeSet` `Sym2.instFintype` `instDecidableRelAdjDeleteIncidenceSet` `Finset.filter` `Sym2` `SetLike.instMembership` `Sym2.instSetLike` `Sym2.Mem.decidable`	—	`edgeFinset_deleteIncidenceSet_eq_sdiff` `Finset.sdiff_eq_filter` `Finset.filter_congr` `incidenceFinset.eq_1` `Set.mem_toFinset` `incidenceSet.eq_1` `Set.mem_setOf_eq` `mem_edgeFinset`
`edgeFinset_deleteIncidenceSet_eq_sdiff` 📖	mathematical	—	`edgeFinset` `deleteIncidenceSet` `fintypeEdgeSet` `Sym2.instFintype` `instDecidableRelAdjDeleteIncidenceSet` `Finset` `Sym2` `Finset.instSDiff` `Sym2.instDecidableEq` `incidenceFinset` `neighborSetFintype`	—	`Finset.coe_injective` `coe_edgeFinset` `Finset.coe_sdiff` `coe_incidenceFinset` `edgeSet_deleteIncidenceSet`
`edgeSet_deleteEdges` 📖	mathematical	—	`edgeSet` `deleteEdges` `Set` `Sym2` `Set.instSDiff`	—	`edgeSet_sdiff` `edgeSet_fromEdgeSet` `edgeSet_sdiff_sdiff_isDiag`
`edgeSet_deleteIncidenceSet` 📖	mathematical	—	`edgeSet` `deleteIncidenceSet` `Set` `Sym2` `Set.instSDiff` `incidenceSet`	—	`edgeSet_sdiff` `edgeSet_fromEdgeSet_incidenceSet`
`edgeSet_fromEdgeSet_incidenceSet` 📖	mathematical	—	`edgeSet` `fromEdgeSet` `incidenceSet`	—	`edgeSet_fromEdgeSet` `sdiff_eq_left` `Set.subset_compl_iff_disjoint_right` `HasSubset.Subset.trans` `Set.instIsTransSubset` `incidenceSet_subset` `edgeSet_subset_compl_diagSet`
`induce_deleteIncidenceSet_of_notMem` 📖	mathematical	`Set` `Set.instMembership`	`induce` `deleteIncidenceSet`	—	`ext` `Membership.mem.ne_of_notMem` `Subtype.prop`
`support_deleteIncidenceSet_subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `support` `deleteIncidenceSet` `Set.instSDiff` `Set.instSingletonSet`	—	—

SimpleGraph.DeleteFar

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_card_edgeFinset` 📖	mathematical	`SimpleGraph.DeleteFar` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `SimpleGraph.completeAtomicBooleanAlgebra`	`Preorder.toLE` `PartialOrder.toPreorder` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Finset.card` `Sym2` `SimpleGraph.edgeFinset`	—	`subset_rfl` `Finset.instReflSubset` `SimpleGraph.coe_edgeFinset` `SimpleGraph.deleteEdges_edgeSet` `sdiff_self`
`le_card_sub_card` 📖	mathematical	`SimpleGraph.DeleteFar` `SimpleGraph` `SimpleGraph.instLE`	`Preorder.toLE` `PartialOrder.toPreorder` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Finset.card` `Sym2` `SimpleGraph.edgeFinset` `SimpleGraph.fintypeEdgeSet`	—	`SimpleGraph.deleteFar_iff`
`mono` 📖	—	`SimpleGraph.DeleteFar` `Preorder.toLE` `PartialOrder.toPreorder`	—	—	`LE.le.trans`

---

← Back to Index