Commit 2023-02-27 11:35 17b46328

View on Github →

feat: port Combinatorics.SimpleGraph.Density (#2492)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SimpleGraph/Density.lean

added theorem Rel.abs_edgeDensity_sub_edgeDensity_le_one_sub_mul

added theorem Rel.abs_edgeDensity_sub_edgeDensity_le_two_mul

added theorem Rel.abs_edgeDensity_sub_edgeDensity_le_two_mul_sub_sq

added theorem Rel.card_interedges_add_card_interedges_compl

added theorem Rel.card_interedges_comm

added theorem Rel.card_interedges_finpartition

added theorem Rel.card_interedges_finpartition_left

added theorem Rel.card_interedges_finpartition_right

added theorem Rel.card_interedges_le_mul

added def Rel.edgeDensity

added theorem Rel.edgeDensity_add_edgeDensity_compl

added theorem Rel.edgeDensity_comm

added theorem Rel.edgeDensity_empty_left

added theorem Rel.edgeDensity_empty_right

added theorem Rel.edgeDensity_le_one

added theorem Rel.edgeDensity_nonneg

added theorem Rel.edgeDensity_sub_edgeDensity_le_one_sub_mul

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

added theorem Rel.swap_mem_interedges_iff

added theorem SimpleGraph.card_interedges_add_card_interedges_compl

added theorem SimpleGraph.card_interedges_div_card

added theorem SimpleGraph.card_interedges_le_mul

added def SimpleGraph.edgeDensity

added theorem SimpleGraph.edgeDensity_add_edgeDensity_compl

added theorem SimpleGraph.edgeDensity_comm

added theorem SimpleGraph.edgeDensity_def

added theorem SimpleGraph.edgeDensity_empty_left

added theorem SimpleGraph.edgeDensity_empty_right

added theorem SimpleGraph.edgeDensity_le_one

added theorem SimpleGraph.edgeDensity_nonneg

added def SimpleGraph.interedges

added theorem SimpleGraph.interedges_bunionᵢ

added theorem SimpleGraph.interedges_bunionᵢ_left

added theorem SimpleGraph.interedges_bunionᵢ_right

added theorem SimpleGraph.interedges_def

added theorem SimpleGraph.interedges_disjoint_left

added theorem SimpleGraph.interedges_disjoint_right

added theorem SimpleGraph.interedges_empty_left

added theorem SimpleGraph.interedges_mono

added theorem SimpleGraph.mem_interedges_iff

added theorem SimpleGraph.mk_mem_interedges_comm

added theorem SimpleGraph.mk_mem_interedges_iff

added theorem SimpleGraph.swap_mem_interedges_iff