Commit 2023-02-27 10:46 e8690948

View on Github →

feat: port Combinatorics.SimpleGraph.Subgraph (#2495)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

added theorem Disjoint.edgeSet

added theorem SimpleGraph.Subgraph.Adj.of_spanningCoe

added def SimpleGraph.Subgraph.IsInduced

added theorem SimpleGraph.Subgraph.IsSpanning.card_verts

added def SimpleGraph.Subgraph.IsSpanning

added def SimpleGraph.Subgraph.IsSubgraph

added theorem SimpleGraph.Subgraph.adj_comm

added theorem SimpleGraph.Subgraph.adj_symm

added def SimpleGraph.Subgraph.bot

added def SimpleGraph.Subgraph.botEquiv

added theorem SimpleGraph.Subgraph.bot_verts

added def SimpleGraph.Subgraph.coeNeighborSetEquiv

added theorem SimpleGraph.Subgraph.coeSubgraph_injective

added theorem SimpleGraph.Subgraph.coe_adj_sub

added theorem SimpleGraph.Subgraph.coe_degree

added theorem SimpleGraph.Subgraph.coe_deleteEdges_eq

added theorem SimpleGraph.Subgraph.coe_deleteEdges_le

added theorem SimpleGraph.Subgraph.comap_monotone

added def SimpleGraph.Subgraph.copy

added theorem SimpleGraph.Subgraph.copy_eq

added def SimpleGraph.Subgraph.degree

added theorem SimpleGraph.Subgraph.degree_eq_one_iff_unique_adj

added theorem SimpleGraph.Subgraph.degree_le'

added theorem SimpleGraph.Subgraph.degree_le

added theorem SimpleGraph.Subgraph.degree_spanningCoe

added def SimpleGraph.Subgraph.deleteEdges

added theorem SimpleGraph.Subgraph.deleteEdges_adj

added theorem SimpleGraph.Subgraph.deleteEdges_coe_eq

added theorem SimpleGraph.Subgraph.deleteEdges_deleteEdges

added theorem SimpleGraph.Subgraph.deleteEdges_empty_eq

added theorem SimpleGraph.Subgraph.deleteEdges_inter_edgeSet_left_eq

added theorem SimpleGraph.Subgraph.deleteEdges_inter_edgeSet_right_eq

added theorem SimpleGraph.Subgraph.deleteEdges_le

added theorem SimpleGraph.Subgraph.deleteEdges_le_of_le

added theorem SimpleGraph.Subgraph.deleteEdges_spanningCoe_eq

added theorem SimpleGraph.Subgraph.deleteEdges_verts

added def SimpleGraph.Subgraph.deleteVerts

added theorem SimpleGraph.Subgraph.deleteVerts_adj

added theorem SimpleGraph.Subgraph.deleteVerts_anti

added theorem SimpleGraph.Subgraph.deleteVerts_deleteVerts

added theorem SimpleGraph.Subgraph.deleteVerts_empty

added theorem SimpleGraph.Subgraph.deleteVerts_inter_verts_left_eq

added theorem SimpleGraph.Subgraph.deleteVerts_inter_verts_set_right_eq

added theorem SimpleGraph.Subgraph.deleteVerts_le

added theorem SimpleGraph.Subgraph.deleteVerts_mono

added theorem SimpleGraph.Subgraph.deleteVerts_verts

added def SimpleGraph.Subgraph.edgeSet

added theorem SimpleGraph.Subgraph.edgeSet_bot

added theorem SimpleGraph.Subgraph.edgeSet_inf

added theorem SimpleGraph.Subgraph.edgeSet_mono

added theorem SimpleGraph.Subgraph.edgeSet_subset

added theorem SimpleGraph.Subgraph.edgeSet_sup

added theorem SimpleGraph.Subgraph.edgeSet_top

added def SimpleGraph.Subgraph.finiteAtOfSubgraph

added theorem SimpleGraph.Subgraph.finset_card_neighborSet_eq_degree

added theorem SimpleGraph.Subgraph.hom.injective

added def SimpleGraph.Subgraph.incidenceSet

added theorem SimpleGraph.Subgraph.incidenceSet_subset

added theorem SimpleGraph.Subgraph.incidenceSet_subset_incidenceSet

added theorem SimpleGraph.Subgraph.inclusion.injective

added def SimpleGraph.Subgraph.inclusion

added def SimpleGraph.Subgraph.induce

added theorem SimpleGraph.Subgraph.induce_empty

added theorem SimpleGraph.Subgraph.induce_mono

added theorem SimpleGraph.Subgraph.induce_mono_left

added theorem SimpleGraph.Subgraph.induce_mono_right

added theorem SimpleGraph.Subgraph.induce_self_verts

added theorem SimpleGraph.Subgraph.inf_adj

added def SimpleGraph.Subgraph.inter

added theorem SimpleGraph.Subgraph.isSpanning_iff

added theorem SimpleGraph.Subgraph.map_le_iff_le_comap

added theorem SimpleGraph.Subgraph.map_monotone

added theorem SimpleGraph.Subgraph.map_sup

added theorem SimpleGraph.Subgraph.mem_edgeSet

added theorem SimpleGraph.Subgraph.mem_neighborSet

added theorem SimpleGraph.Subgraph.mem_support

added theorem SimpleGraph.Subgraph.mem_verts_if_mem_edge

added def SimpleGraph.Subgraph.neighborSet

added theorem SimpleGraph.Subgraph.neighborSet_inf

added theorem SimpleGraph.Subgraph.neighborSet_subset

added theorem SimpleGraph.Subgraph.neighborSet_subset_of_subgraph

added theorem SimpleGraph.Subgraph.neighborSet_subset_verts

added theorem SimpleGraph.Subgraph.neighborSet_sup

added theorem SimpleGraph.Subgraph.not_bot_adj

added theorem SimpleGraph.Subgraph.restrict_coeSubgraph

added theorem SimpleGraph.Subgraph.singletonSubgraph_eq_induce

added def SimpleGraph.Subgraph.spanningCoeEquivCoeOfSpanning

added theorem SimpleGraph.Subgraph.spanningCoe_bot

added theorem SimpleGraph.Subgraph.spanningCoe_deleteEdges_le

added theorem SimpleGraph.Subgraph.spanningCoe_le_of_le

added theorem SimpleGraph.Subgraph.spanningCoe_top

added theorem SimpleGraph.Subgraph.spanningHom.injective

added def SimpleGraph.Subgraph.spanningHom

added theorem SimpleGraph.Subgraph.subgraphOfAdj_eq_induce

added theorem SimpleGraph.Subgraph.sup_adj

added def SimpleGraph.Subgraph.support

added theorem SimpleGraph.Subgraph.support_mono

added theorem SimpleGraph.Subgraph.support_subset_verts

added def SimpleGraph.Subgraph.top

added def SimpleGraph.Subgraph.topEquiv

added theorem SimpleGraph.Subgraph.top_adj_iff

added theorem SimpleGraph.Subgraph.top_verts

added def SimpleGraph.Subgraph.union

added def SimpleGraph.Subgraph.vert

added theorem SimpleGraph.Subgraph.verts_inf

added theorem SimpleGraph.Subgraph.verts_sup

added structure SimpleGraph.Subgraph

added theorem SimpleGraph.edgeSet_singletonSubgraph

added theorem SimpleGraph.edgeSet_subgraphOfAdj

added theorem SimpleGraph.eq_singletonSubgraph_iff_verts_eq

added theorem SimpleGraph.induce_eq_coe_induce_top

added theorem SimpleGraph.map_singletonSubgraph

added theorem SimpleGraph.map_subgraphOfAdj

added theorem SimpleGraph.neighborSet_fst_subgraphOfAdj

added theorem SimpleGraph.neighborSet_singletonSubgraph

added theorem SimpleGraph.neighborSet_snd_subgraphOfAdj

added theorem SimpleGraph.neighborSet_subgraphOfAdj

added theorem SimpleGraph.neighborSet_subgraphOfAdj_of_ne_of_ne

added theorem SimpleGraph.neighborSet_subgraphOfAdj_subset

added theorem SimpleGraph.singletonSubgraph_fst_le_subgraphOfAdj

added theorem SimpleGraph.singletonSubgraph_le_iff

added theorem SimpleGraph.singletonSubgraph_snd_le_subgraphOfAdj

added def SimpleGraph.subgraphOfAdj

added theorem SimpleGraph.subgraphOfAdj_symm

added theorem SimpleGraph.toSubgraph.isSpanning

added def SimpleGraph.toSubgraph