Commit 2024-01-09 07:49 c147cdfc

View on Github →

refactor: split graph maps into a new file (#9579) A continuation from https://github.com/leanprover-community/mathlib4/pull/9267#discussion_r1437052000.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

deleted theorem Equiv.simpleGraph_refl

deleted theorem Equiv.simpleGraph_trans

deleted theorem Equiv.symm_simpleGraph

deleted theorem SimpleGraph.Embedding.apply_mem_neighborSet_iff

deleted theorem SimpleGraph.Embedding.coe_comp

deleted theorem SimpleGraph.Embedding.coe_toHom

deleted theorem SimpleGraph.Embedding.comap_apply

deleted def SimpleGraph.Embedding.mapEdgeSet

deleted def SimpleGraph.Embedding.mapNeighborSet

deleted theorem SimpleGraph.Embedding.map_adj_iff

deleted theorem SimpleGraph.Embedding.map_apply

deleted theorem SimpleGraph.Embedding.map_mem_edgeSet_iff

deleted theorem SimpleGraph.Hom.apply_mem_neighborSet

deleted theorem SimpleGraph.Hom.coe_comp

deleted theorem SimpleGraph.Hom.coe_id

deleted theorem SimpleGraph.Hom.coe_ofLe

deleted theorem SimpleGraph.Hom.injective_of_top_hom

deleted def SimpleGraph.Hom.mapDart

deleted theorem SimpleGraph.Hom.mapDart_apply

deleted theorem SimpleGraph.Hom.mapEdgeSet.injective

deleted def SimpleGraph.Hom.mapEdgeSet

deleted def SimpleGraph.Hom.mapNeighborSet

deleted def SimpleGraph.Hom.mapSpanningSubgraphs

deleted theorem SimpleGraph.Hom.map_adj

deleted theorem SimpleGraph.Hom.map_mem_edgeSet

deleted def SimpleGraph.Hom.ofLe

deleted theorem SimpleGraph.Iso.apply_mem_neighborSet_iff

deleted theorem SimpleGraph.Iso.card_eq_of_iso

deleted theorem SimpleGraph.Iso.coe_comp

deleted theorem SimpleGraph.Iso.comap_apply

deleted theorem SimpleGraph.Iso.comap_symm_apply

deleted def SimpleGraph.Iso.mapEdgeSet

deleted def SimpleGraph.Iso.mapNeighborSet

deleted theorem SimpleGraph.Iso.map_adj_iff

deleted theorem SimpleGraph.Iso.map_apply

deleted theorem SimpleGraph.Iso.map_mem_edgeSet_iff

deleted theorem SimpleGraph.Iso.map_symm_apply

deleted theorem SimpleGraph.Iso.toEmbedding_completeGraph

deleted theorem SimpleGraph.coe_induceHom

deleted theorem SimpleGraph.comap_adj

deleted theorem SimpleGraph.comap_comap

deleted theorem SimpleGraph.comap_id

deleted theorem SimpleGraph.comap_map_eq

deleted theorem SimpleGraph.comap_monotone

deleted theorem SimpleGraph.comap_surjective

deleted theorem SimpleGraph.comap_symm

deleted def SimpleGraph.induce

deleted def SimpleGraph.induceHom

deleted def SimpleGraph.induceHomOfLE

deleted theorem SimpleGraph.induceHomOfLE_apply

deleted theorem SimpleGraph.induceHomOfLE_toHom

deleted theorem SimpleGraph.induceHom_comp

deleted theorem SimpleGraph.induceHom_id

deleted theorem SimpleGraph.induceHom_injective

deleted def SimpleGraph.induceUnivIso

deleted theorem SimpleGraph.induce_singleton_eq_top

deleted theorem SimpleGraph.induce_spanningCoe

deleted theorem SimpleGraph.le_comap_of_subsingleton

deleted theorem SimpleGraph.leftInverse_comap_map

deleted theorem SimpleGraph.map_adj

deleted theorem SimpleGraph.map_adj_apply

deleted theorem SimpleGraph.map_comap_le

deleted theorem SimpleGraph.map_id

deleted theorem SimpleGraph.map_injective

deleted theorem SimpleGraph.map_le_iff_le_comap

deleted theorem SimpleGraph.map_le_of_subsingleton

deleted theorem SimpleGraph.map_map

deleted theorem SimpleGraph.map_monotone

deleted theorem SimpleGraph.map_symm

deleted def SimpleGraph.spanningCoe

deleted theorem SimpleGraph.spanningCoe_induce_le

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

Created Mathlib/Combinatorics/SimpleGraph/Maps.lean

added theorem Equiv.simpleGraph_refl

added theorem Equiv.simpleGraph_trans

added theorem Equiv.symm_simpleGraph

added theorem SimpleGraph.Embedding.apply_mem_neighborSet_iff

added theorem SimpleGraph.Embedding.coe_comp

added theorem SimpleGraph.Embedding.coe_toHom

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.coe_id

added theorem SimpleGraph.Hom.coe_ofLe

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.Hom.ofLe

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 theorem SimpleGraph.coe_induceHom

added theorem SimpleGraph.comap_adj

added theorem SimpleGraph.comap_comap

added theorem SimpleGraph.comap_id

added theorem SimpleGraph.comap_map_eq

added theorem SimpleGraph.comap_monotone

added theorem SimpleGraph.comap_surjective

added theorem SimpleGraph.comap_symm

added def SimpleGraph.induce

added def SimpleGraph.induceHom

added def SimpleGraph.induceHomOfLE

added theorem SimpleGraph.induceHomOfLE_apply

added theorem SimpleGraph.induceHomOfLE_toHom

added theorem SimpleGraph.induceHom_comp

added theorem SimpleGraph.induceHom_id

added theorem SimpleGraph.induceHom_injective

added def SimpleGraph.induceUnivIso

added theorem SimpleGraph.induce_singleton_eq_top

added theorem SimpleGraph.induce_spanningCoe

added theorem SimpleGraph.le_comap_of_subsingleton

added theorem SimpleGraph.leftInverse_comap_map

added theorem SimpleGraph.map_adj

added theorem SimpleGraph.map_adj_apply

added theorem SimpleGraph.map_comap_le

added theorem SimpleGraph.map_id

added theorem SimpleGraph.map_injective

added theorem SimpleGraph.map_le_iff_le_comap

added theorem SimpleGraph.map_le_of_subsingleton

added theorem SimpleGraph.map_map

added theorem SimpleGraph.map_monotone

added theorem SimpleGraph.map_symm

added def SimpleGraph.spanningCoe

added theorem SimpleGraph.spanningCoe_induce_le

Modified Mathlib/Combinatorics/SimpleGraph/Subgraph.lean