Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-15 18:06 e3a8dff0

View on Github →

feat(combinatorics/simple_graph/*): some more from_edge_set and edge_set lemmas (#17723)

Estimated changes

Modified src/combinatorics/simple_graph/basic.lean

modified theorem simple_graph.coe_edge_finset

modified def simple_graph.edge_finset

added theorem simple_graph.edge_finset_bot

modified theorem simple_graph.edge_finset_card

added theorem simple_graph.edge_finset_inf

added theorem simple_graph.edge_finset_inj

deleted theorem simple_graph.edge_finset_mono

added theorem simple_graph.edge_finset_sdiff

added theorem simple_graph.edge_finset_ssubset_edge_finset

added theorem simple_graph.edge_finset_subset_edge_finset

added theorem simple_graph.edge_finset_sup

modified def simple_graph.edge_set

added theorem simple_graph.edge_set_bot

modified theorem simple_graph.edge_set_from_edge_set

added theorem simple_graph.edge_set_inf

added theorem simple_graph.edge_set_inj

added theorem simple_graph.edge_set_injective

deleted theorem simple_graph.edge_set_mono

added theorem simple_graph.edge_set_sdiff

added theorem simple_graph.edge_set_sdiff_sdiff_is_diag

added theorem simple_graph.edge_set_ssubset_edge_set

added theorem simple_graph.edge_set_subset_edge_set

added theorem simple_graph.edge_set_sup

modified theorem simple_graph.edge_set_univ_card

added theorem simple_graph.from_edge_set_inf

added theorem simple_graph.from_edge_set_mono

added theorem simple_graph.from_edge_set_sdiff

added theorem simple_graph.from_edge_set_sup

modified theorem simple_graph.mem_edge_finset

added theorem simple_graph.not_is_diag_of_mem_edge_finset

added theorem simple_graph.not_is_diag_of_mem_edge_set

Modified src/combinatorics/simple_graph/connectivity.lean

Modified src/data/fintype/basic.lean

modified theorem set.to_finset_compl

modified theorem set.to_finset_diff

modified theorem set.to_finset_inter

modified theorem set.to_finset_union