Commit 2022-03-24 16:39 6ac7c18d

View on Github →

feat(combinatorics/simple_graph/density): Edge density (#12431) Define the number and density of edges of a relation and of a simple graph between two finsets.

Estimated changes

Created src/combinatorics/simple_graph/density.lean

added theorem rel.card_interedges_add_card_interedges_compl

added theorem rel.card_interedges_comm

added theorem rel.card_interedges_le_mul

added def rel.edge_density

added theorem rel.edge_density_add_edge_density_compl

added theorem rel.edge_density_comm

added theorem rel.edge_density_empty_left

added theorem rel.edge_density_empty_right

added theorem rel.edge_density_le_one

added theorem rel.edge_density_nonneg

added def rel.interedges

added theorem rel.interedges_bUnion

added theorem rel.interedges_bUnion_left

added theorem rel.interedges_bUnion_right

added theorem rel.interedges_disjoint_left

added theorem rel.interedges_disjoint_right

added theorem rel.interedges_empty_left

added theorem rel.interedges_mono

added theorem rel.mem_interedges_iff

added theorem rel.mk_mem_interedges_comm

added theorem rel.mk_mem_interedges_iff

added theorem rel.swap_mem_interedges_iff

added theorem simple_graph.card_interedges_add_card_interedges_compl

added theorem simple_graph.card_interedges_div_card

added theorem simple_graph.card_interedges_le_mul

added def simple_graph.edge_density

added theorem simple_graph.edge_density_add_edge_density_compl

added theorem simple_graph.edge_density_comm

added theorem simple_graph.edge_density_def

added theorem simple_graph.edge_density_empty_left

added theorem simple_graph.edge_density_empty_right

added theorem simple_graph.edge_density_le_one

added theorem simple_graph.edge_density_nonneg

added def simple_graph.interedges

added theorem simple_graph.interedges_bUnion

added theorem simple_graph.interedges_bUnion_left

added theorem simple_graph.interedges_bUnion_right

added theorem simple_graph.interedges_def

added theorem simple_graph.interedges_disjoint_left

added theorem simple_graph.interedges_disjoint_right

added theorem simple_graph.interedges_empty_left

added theorem simple_graph.interedges_mono

added theorem simple_graph.mem_interedges_iff

added theorem simple_graph.mk_mem_interedges_comm

added theorem simple_graph.mk_mem_interedges_iff

added theorem simple_graph.swap_mem_interedges_iff