Commit 2023-02-24 18:27 871dcdaa

View on Github →

feat: Port Combinatorics.SimpleGraph.Basic (#1883)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SimpleGraph/Basic.lean

added theorem SimpleGraph.Adj.card_commonNeighbors_lt_degree

added theorem SimpleGraph.Adj.symm

added def SimpleGraph.Dart.edge

added theorem SimpleGraph.Dart.edge_comp_symm

added theorem SimpleGraph.Dart.edge_mem

added theorem SimpleGraph.Dart.edge_mk

added theorem SimpleGraph.Dart.edge_symm

added theorem SimpleGraph.Dart.ext

added theorem SimpleGraph.Dart.ext_iff

added def SimpleGraph.Dart.symm

added theorem SimpleGraph.Dart.symm_involutive

added theorem SimpleGraph.Dart.symm_mk

added theorem SimpleGraph.Dart.symm_ne

added theorem SimpleGraph.Dart.symm_symm

added theorem SimpleGraph.Dart.toProd_injective

added structure SimpleGraph.Dart

added def SimpleGraph.DartAdj

added theorem SimpleGraph.DeleteFar.mono

added def SimpleGraph.DeleteFar

added theorem SimpleGraph.Embedding.apply_mem_neighborSet_iff

added theorem SimpleGraph.Embedding.coe_comp

added theorem SimpleGraph.Embedding.comap_apply

added def SimpleGraph.Embedding.mapEdgeSet

added def SimpleGraph.Embedding.mapNeighborSet

added theorem SimpleGraph.Embedding.map_adj_iff

added theorem SimpleGraph.Embedding.map_apply

added theorem SimpleGraph.Embedding.map_mem_edgeSet_iff

added theorem SimpleGraph.Hom.apply_mem_neighborSet

added theorem SimpleGraph.Hom.coe_comp

added theorem SimpleGraph.Hom.injective_of_top_hom

added def SimpleGraph.Hom.mapDart

added theorem SimpleGraph.Hom.mapDart_apply

added theorem SimpleGraph.Hom.mapEdgeSet.injective

added def SimpleGraph.Hom.mapEdgeSet

added def SimpleGraph.Hom.mapNeighborSet

added def SimpleGraph.Hom.mapSpanningSubgraphs

added theorem SimpleGraph.Hom.map_adj

added theorem SimpleGraph.Hom.map_mem_edgeSet

added def SimpleGraph.InduceHom

added theorem SimpleGraph.IsRegularOfDegree.compl

added theorem SimpleGraph.IsRegularOfDegree.degree_eq

added theorem SimpleGraph.IsRegularOfDegree.top

added def SimpleGraph.IsRegularOfDegree

added def SimpleGraph.IsSubgraph

added theorem SimpleGraph.Iso.apply_mem_neighborSet_iff

added theorem SimpleGraph.Iso.card_eq_of_iso

added theorem SimpleGraph.Iso.coe_comp

added theorem SimpleGraph.Iso.comap_apply

added theorem SimpleGraph.Iso.comap_symm_apply

added def SimpleGraph.Iso.mapEdgeSet

added def SimpleGraph.Iso.mapNeighborSet

added theorem SimpleGraph.Iso.map_adj_iff

added theorem SimpleGraph.Iso.map_apply

added theorem SimpleGraph.Iso.map_mem_edgeSet_iff

added theorem SimpleGraph.Iso.map_symm_apply

added theorem SimpleGraph.Iso.toEmbedding_completeGraph

added def SimpleGraph.LocallyFinite

added theorem SimpleGraph.adj_comm

added theorem SimpleGraph.adj_iff_exists_edge

added theorem SimpleGraph.adj_iff_exists_edge_coe

added theorem SimpleGraph.adj_incidenceSet_inter

added theorem SimpleGraph.adj_of_mem_incidenceSet

added theorem SimpleGraph.adj_symm

added theorem SimpleGraph.bot_adj

added theorem SimpleGraph.bot_degree

added theorem SimpleGraph.card_commonNeighbors_le_degree_left

added theorem SimpleGraph.card_commonNeighbors_le_degree_right

added theorem SimpleGraph.card_commonNeighbors_lt_card_verts

added theorem SimpleGraph.card_commonNeighbors_top

added theorem SimpleGraph.card_incidenceFinset_eq_degree

added theorem SimpleGraph.card_incidenceSet_eq_degree

added theorem SimpleGraph.card_neighborSet_eq_degree

added theorem SimpleGraph.card_neighborSet_union_compl_neighborSet

added theorem SimpleGraph.coe_edgeFinset

added theorem SimpleGraph.coe_induceHom

added theorem SimpleGraph.comap_map_eq

added theorem SimpleGraph.comap_monotone

added theorem SimpleGraph.comap_surjective

added def SimpleGraph.commonNeighbors

added theorem SimpleGraph.commonNeighbors_eq

added theorem SimpleGraph.commonNeighbors_subset_neighborSet_left

added theorem SimpleGraph.commonNeighbors_subset_neighborSet_right

added theorem SimpleGraph.commonNeighbors_symm

added theorem SimpleGraph.commonNeighbors_top_eq

added theorem SimpleGraph.compl_adj

added theorem SimpleGraph.compl_eq_deleteEdges

added theorem SimpleGraph.compl_neighborSet_disjoint

added theorem SimpleGraph.completeGraph_eq_top

added theorem SimpleGraph.complete_graph_degree

added def SimpleGraph.dartOfNeighborSet

added theorem SimpleGraph.dartOfNeighborSet_injective

added theorem SimpleGraph.dart_edge_eq_iff

added theorem SimpleGraph.dart_edge_eq_mk'_iff'

added theorem SimpleGraph.dart_edge_eq_mk'_iff

added def SimpleGraph.degree

added theorem SimpleGraph.degree_compl

added theorem SimpleGraph.degree_le_maxDegree

added theorem SimpleGraph.degree_lt_card_verts

added theorem SimpleGraph.degree_pos_iff_exists_adj

added def SimpleGraph.deleteEdges

added theorem SimpleGraph.deleteEdges_adj

added theorem SimpleGraph.deleteEdges_deleteEdges

added theorem SimpleGraph.deleteEdges_empty_eq

added theorem SimpleGraph.deleteEdges_eq_inter_edgeSet

added theorem SimpleGraph.deleteEdges_eq_sdiff_fromEdgeSet

added theorem SimpleGraph.deleteEdges_le

added theorem SimpleGraph.deleteEdges_le_of_le

added theorem SimpleGraph.deleteEdges_sdiff_eq_of_le

added theorem SimpleGraph.deleteEdges_univ_eq

added theorem SimpleGraph.deleteFar_iff

added def SimpleGraph.edgeFinset

added theorem SimpleGraph.edgeFinset_bot

added theorem SimpleGraph.edgeFinset_card

added theorem SimpleGraph.edgeFinset_deleteEdges

added theorem SimpleGraph.edgeFinset_inf

added theorem SimpleGraph.edgeFinset_inj

added theorem SimpleGraph.edgeFinset_sSubset_edgeFinset

added theorem SimpleGraph.edgeFinset_sdiff

added theorem SimpleGraph.edgeFinset_subset_edgeFinset

added theorem SimpleGraph.edgeFinset_sup

added def SimpleGraph.edgeSetEmbedding

added theorem SimpleGraph.edgeSet_bot

added theorem SimpleGraph.edgeSet_deleteEdges

added theorem SimpleGraph.edgeSet_fromEdgeSet

added theorem SimpleGraph.edgeSet_inf

added theorem SimpleGraph.edgeSet_inj

added theorem SimpleGraph.edgeSet_injective

added theorem SimpleGraph.edgeSet_sSubset_edgeSet

added theorem SimpleGraph.edgeSet_sdiff

added theorem SimpleGraph.edgeSet_sdiff_sdiff_isDiag

added theorem SimpleGraph.edgeSet_subset_edgeSet

added theorem SimpleGraph.edgeSet_sup

added theorem SimpleGraph.edgeSet_univ_card

added theorem SimpleGraph.edge_mem_incidenceSet_iff

added theorem SimpleGraph.edge_other_incident_set

added theorem SimpleGraph.edge_other_ne

added theorem SimpleGraph.emptyGraph_eq_bot

added theorem SimpleGraph.exists_maximal_degree_vertex

added theorem SimpleGraph.exists_minimal_degree_vertex

added def SimpleGraph.fromEdgeSet

added theorem SimpleGraph.fromEdgeSet_adj

added theorem SimpleGraph.fromEdgeSet_edgeSet

added theorem SimpleGraph.fromEdgeSet_empty

added theorem SimpleGraph.fromEdgeSet_inf

added theorem SimpleGraph.fromEdgeSet_mono

added theorem SimpleGraph.fromEdgeSet_sdiff

added theorem SimpleGraph.fromEdgeSet_sup

added theorem SimpleGraph.fromEdgeSet_univ

added def SimpleGraph.fromRel

added theorem SimpleGraph.fromRel_adj

added def SimpleGraph.incidenceFinset

added theorem SimpleGraph.incidenceFinset_eq_filter

added def SimpleGraph.incidenceSet

added def SimpleGraph.incidenceSetEquivNeighborSet

added theorem SimpleGraph.incidenceSet_inter_incidenceSet_of_adj

added theorem SimpleGraph.incidenceSet_inter_incidenceSet_of_not_adj

added theorem SimpleGraph.incidenceSet_inter_incidenceSet_subset

added theorem SimpleGraph.incidenceSet_subset

added theorem SimpleGraph.incidence_other_neighbor_edge

added theorem SimpleGraph.incidence_other_prop

added def SimpleGraph.induce

added theorem SimpleGraph.induceHom_comp

added theorem SimpleGraph.induceHom_id

added theorem SimpleGraph.induce_spanningCoe

added theorem SimpleGraph.inf_adj

added theorem SimpleGraph.isSubgraph_eq_le

added theorem SimpleGraph.le_minDegree_of_forall_le_degree

added theorem SimpleGraph.leftInverse_comap_map

added theorem SimpleGraph.map_adj

added theorem SimpleGraph.map_comap_le

added theorem SimpleGraph.map_injective

added theorem SimpleGraph.map_le_iff_le_comap

added theorem SimpleGraph.map_monotone

added def SimpleGraph.maxDegree

added theorem SimpleGraph.maxDegree_le_of_forall_degree_le

added theorem SimpleGraph.maxDegree_lt_card_verts

added theorem SimpleGraph.mem_commonNeighbors

added theorem SimpleGraph.mem_edgeFinset

added theorem SimpleGraph.mem_edgeSet

added theorem SimpleGraph.mem_incidenceFinset

added theorem SimpleGraph.mem_incidenceSet

added theorem SimpleGraph.mem_incidence_iff_neighbor

added theorem SimpleGraph.mem_neighborFinset

added theorem SimpleGraph.mem_neighborSet

added theorem SimpleGraph.mem_support

added def SimpleGraph.minDegree

added theorem SimpleGraph.minDegree_le_degree

added theorem SimpleGraph.mk'_mem_incidenceSet_iff

added theorem SimpleGraph.mk'_mem_incidenceSet_left_iff

added theorem SimpleGraph.mk'_mem_incidenceSet_right_iff

added theorem SimpleGraph.ne_of_adj

added theorem SimpleGraph.ne_of_adj_of_not_adj

added def SimpleGraph.neighborFinset

added theorem SimpleGraph.neighborFinset_compl

added theorem SimpleGraph.neighborFinset_def

added theorem SimpleGraph.neighborFinset_disjoint_singleton

added theorem SimpleGraph.neighborFinset_eq_filter

added def SimpleGraph.neighborSet

added theorem SimpleGraph.neighborSet_compl

added theorem SimpleGraph.neighborSet_union_compl_neighborSet_eq

added theorem SimpleGraph.not_isDiag_of_mem_edgeFinset

added theorem SimpleGraph.not_isDiag_of_mem_edgeSet

added theorem SimpleGraph.not_mem_commonNeighbors_left

added theorem SimpleGraph.not_mem_commonNeighbors_right

added theorem SimpleGraph.not_mem_neighborFinset_self

added def SimpleGraph.otherVertexOfIncident

added theorem SimpleGraph.sdiff_adj

added theorem SimpleGraph.sdiff_eq_deleteEdges

added theorem SimpleGraph.singleton_disjoint_neighborFinset

added def SimpleGraph.spanningCoe

added theorem SimpleGraph.spanningCoe_induce_le

added theorem SimpleGraph.sup_adj

added def SimpleGraph.support

added theorem SimpleGraph.support_mono

added theorem SimpleGraph.top_adj

added structure SimpleGraph

added def completeBipartiteGraph

added def completeGraph

added def emptyGraph