Density

📁 Source: Mathlib/Combinatorics/SimpleGraph/Density.lean

Statistics

Metric	Count
Definitions edgeDensity, interedges, edgeDensity, interedges	4
Theorems abs_edgeDensity_sub_edgeDensity_le_one_sub_mul, abs_edgeDensity_sub_edgeDensity_le_two_mul, abs_edgeDensity_sub_edgeDensity_le_two_mul_sub_sq, card_interedges_add_card_interedges_compl, card_interedges_comm, card_interedges_finpartition, card_interedges_finpartition_left, card_interedges_finpartition_right, card_interedges_le_mul, edgeDensity_add_edgeDensity_compl, edgeDensity_comm, edgeDensity_empty_left, edgeDensity_empty_right, edgeDensity_le_one, edgeDensity_nonneg, edgeDensity_sub_edgeDensity_le_one_sub_mul, interedges_biUnion, interedges_biUnion_left, interedges_biUnion_right, interedges_disjoint_left, interedges_disjoint_right, interedges_empty_left, interedges_eq_biUnion, interedges_mono, mem_interedges_iff, mk_mem_interedges_comm, mk_mem_interedges_iff, mul_edgeDensity_le_edgeDensity, swap_mem_interedges_iff, card_interedges_add_card_interedges_compl, card_interedges_div_card, card_interedges_le_mul, edgeDensity_add_edgeDensity_compl, edgeDensity_comm, edgeDensity_def, edgeDensity_empty_left, edgeDensity_empty_right, edgeDensity_le_one, edgeDensity_nonneg, interedges_biUnion, interedges_biUnion_left, interedges_biUnion_right, interedges_def, interedges_disjoint_left, interedges_disjoint_right, interedges_empty_left, interedges_mono, mem_interedges_iff, mk_mem_interedges_comm, mk_mem_interedges_iff, swap_mem_interedges_iff	51
Total	55

Rel

Definitions

Name	Category	Theorems
edgeDensity 📖	CompOp	11 math math: edgeDensity_empty_right, abs_edgeDensity_sub_edgeDensity_le_two_mul, edgeDensity_add_edgeDensity_compl, mul_edgeDensity_le_edgeDensity, edgeDensity_comm, edgeDensity_empty_left, abs_edgeDensity_sub_edgeDensity_le_two_mul_sub_sq, abs_edgeDensity_sub_edgeDensity_le_one_sub_mul, edgeDensity_le_one, edgeDensity_sub_edgeDensity_le_one_sub_mul, edgeDensity_nonneg
interedges 📖	CompOp	18 math math: interedges_biUnion, card_interedges_le_mul, interedges_eq_biUnion, mk_mem_interedges_comm, card_interedges_finpartition, interedges_disjoint_left, interedges_empty_left, card_interedges_finpartition_right, interedges_biUnion_left, mem_interedges_iff, interedges_biUnion_right, mk_mem_interedges_iff, interedges_disjoint_right, card_interedges_finpartition_left, interedges_mono, swap_mem_interedges_iff, card_interedges_add_card_interedges_compl, card_interedges_comm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_edgeDensity_sub_edgeDensity_le_one_sub_mul 📖	mathematical	Finset Finset.instHasSubset Finset.Nonempty	abs Rat.instLattice Rat.addGroup edgeDensity Finset.card	—	abs_sub_le_iff Rat.instIsOrderedAddMonoid edgeDensity_sub_edgeDensity_le_one_sub_mul add_sub_cancel_right edgeDensity_add_edgeDensity_compl Finset.Nonempty.mono sub_sub_sub_cancel_left
abs_edgeDensity_sub_edgeDensity_le_two_mul 📖	mathematical	Finset Finset.instHasSubset Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne AddMonoidWithOne.toNatCast Finset.card	abs DivisionRing.toRatCast edgeDensity instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat lt_or_ge LE.le.trans abs_edgeDensity_sub_edgeDensity_le_two_mul_sub_sq sub_le_self_iff IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono two_mul abs_sub add_le_add covariant_swap_add_of_covariant_add le_trans abs_of_nonneg Nat.cast_zero edgeDensity_nonneg Nat.cast_one edgeDensity_le_one
abs_edgeDensity_sub_edgeDensity_le_two_mul_sub_sq 📖	mathematical	Finset Finset.instHasSubset Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Preorder.toLT AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup AddMonoidWithOne.toNatCast Finset.card	abs DivisionRing.toRatCast edgeDensity instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	Nat.instAtLeastTwoHAddOfNat sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing sq mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono LE.le.trans LT.lt.le IsStrictOrderedRing.toZeroLEOneClass IsStrictOrderedRing.toCharZero Finset.eq_empty_or_nonempty interedges_empty_left Nat.cast_zero MulZeroClass.zero_mul div_zero Rat.cast_zero Rat.cast_div Rat.cast_natCast Rat.cast_mul LE.le.antisymm nonpos_of_mul_nonpos_right IsStrictOrderedRing.toPosMulStrictMono Finset.card_empty sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd Nat.cast_nonneg sub_self abs_zero MulZeroClass.mul_zero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Nat.cast_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Rat.cast_le abs_edgeDensity_sub_edgeDensity_le_one_sub_mul Rat.cast_sub Rat.cast_one Finset.Nonempty.mono sub_le_sub_left mul_le_mul IsOrderedRing.toPosMulMono le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Finset.Nonempty.card_pos le_of_lt div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Nat.cast_pos' NeZero.charZero_one
card_interedges_add_card_interedges_compl 📖	mathematical	—	Finset.card interedges	—	Finset.card_product interedges.eq_1 Finset.card_union_of_disjoint Finset.disjoint_filter Finset.filter_union_filter_not_eq
card_interedges_comm 📖	mathematical	Symmetric	Finset.card interedges	—	Finset.card_bij swap_mem_interedges_iff Prod.swap_injective
card_interedges_finpartition 📖	mathematical	—	Finset.card interedges Finset.sum Finset Nat.instAddCommMonoid SProd.sprod Finset.instSProd Finpartition.parts Finset.instLattice Finset.instOrderBot	—	card_interedges_finpartition_left Finset.sum_product card_interedges_finpartition_right
card_interedges_finpartition_left 📖	mathematical	—	Finset.card interedges Finset.sum Finset Nat.instAddCommMonoid Finpartition.parts Finset.instLattice Finset.instOrderBot	—	interedges.congr_simp Finpartition.biUnion_parts interedges_biUnion_left Finset.card_biUnion interedges_disjoint_left Finpartition.disjoint
card_interedges_finpartition_right 📖	mathematical	—	Finset.card interedges Finset.sum Finset Nat.instAddCommMonoid Finpartition.parts Finset.instLattice Finset.instOrderBot	—	interedges.congr_simp Finpartition.biUnion_parts interedges_biUnion_right Finset.card_biUnion interedges_disjoint_right Finpartition.disjoint
card_interedges_le_mul 📖	mathematical	—	Finset.card interedges	—	LE.le.trans Finset.card_filter_le Eq.le Finset.card_product
edgeDensity_add_edgeDensity_compl 📖	mathematical	Finset.Nonempty	edgeDensity	—	edgeDensity.eq_1 add_div div_eq_one_iff_eq Nat.cast_zero Rat.instCharZero LT.lt.ne' mul_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono Finset.Nonempty.card_pos card_interedges_add_card_interedges_compl
edgeDensity_comm 📖	mathematical	Symmetric	edgeDensity	—	edgeDensity.eq_1 mul_comm card_interedges_comm
edgeDensity_empty_left 📖	mathematical	—	edgeDensity Finset Finset.instEmptyCollection	—	edgeDensity.eq_1 Finset.card_empty Nat.cast_zero MulZeroClass.zero_mul div_zero
edgeDensity_empty_right 📖	mathematical	—	edgeDensity Finset Finset.instEmptyCollection	—	edgeDensity.eq_1 Finset.card_empty Nat.cast_zero MulZeroClass.mul_zero div_zero
edgeDensity_le_one 📖	mathematical	—	edgeDensity	—	div_le_one_of_le₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Rat.instIsStrictOrderedRing Rat.instZeroLEOneClass Rat.instAddLeftMono Rat.instCharZero card_interedges_le_mul Nat.cast_zero
edgeDensity_nonneg 📖	mathematical	—	edgeDensity	—	div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Rat.instIsStrictOrderedRing Nat.cast_zero Rat.instAddLeftMono Rat.instZeroLEOneClass Rat.instCharZero
edgeDensity_sub_edgeDensity_le_one_sub_mul 📖	mathematical	Finset Finset.instHasSubset Finset.Nonempty	edgeDensity Finset.card	—	LE.le.trans sub_le_sub_left Rat.instAddLeftMono covariant_swap_add_of_covariant_add mul_edgeDensity_le_edgeDensity le_trans sub_mul one_mul le_refl mul_le_of_le_one_right Rat.instPosMulMono sub_nonneg_of_le mul_le_one₀ IsOrderedRing.toMulPosMono IsStrictOrderedRing.toIsOrderedRing Rat.instIsStrictOrderedRing div_le_one_of_le₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Rat.instZeroLEOneClass Nat.cast_le Rat.instCharZero Finset.card_le_card Nat.cast_nonneg div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Nat.cast_zero edgeDensity_le_one
interedges_biUnion 📖	mathematical	—	interedges Finset.biUnion SProd.sprod Finset Finset.instSProd	—	Finset.product_biUnion interedges_biUnion_left interedges_biUnion_right
interedges_biUnion_left 📖	mathematical	—	interedges Finset.biUnion	—	Finset.ext
interedges_biUnion_right 📖	mathematical	—	interedges Finset.biUnion	—	Finset.ext
interedges_disjoint_left 📖	mathematical	Disjoint Finset Finset.partialOrder Finset.instOrderBot	interedges	—	Finset.disjoint_left mem_interedges_iff
interedges_disjoint_right 📖	mathematical	Disjoint Finset Finset.partialOrder Finset.instOrderBot	interedges	—	Finset.disjoint_left mem_interedges_iff
interedges_empty_left 📖	mathematical	—	interedges Finset Finset.instEmptyCollection	—	interedges.eq_1 Finset.empty_product Finset.filter_empty
interedges_eq_biUnion 📖	mathematical	—	interedges Finset.biUnion Finset.map Prod.mk_right_injective Finset.filter	—	Finset.ext Prod.mk_right_injective
interedges_mono 📖	mathematical	Finset Finset.instHasSubset	interedges	—	—
mem_interedges_iff 📖	mathematical	—	Finset Finset.instMembership interedges	—	interedges.eq_1 Finset.mem_filter Finset.mem_product
mk_mem_interedges_comm 📖	mathematical	Symmetric	Finset Finset.instMembership interedges	—	swap_mem_interedges_iff
mk_mem_interedges_iff 📖	mathematical	—	Finset Finset.instMembership interedges	—	mem_interedges_iff
mul_edgeDensity_le_edgeDensity 📖	mathematical	Finset Finset.instHasSubset Finset.Nonempty	Finset.card edgeDensity	—	IsStrictOrderedRing.noZeroDivisors Rat.instIsStrictOrderedRing AddGroup.existsAddOfLE Rat.instCharZero Finset.Nonempty.ne_empty edgeDensity.eq_1 div_mul_div_comm mul_comm div_mul_div_cancel₀ div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Nat.mono_cast Rat.instAddLeftMono Rat.instZeroLEOneClass Finset.card_le_card interedges_mono mul_nonneg Rat.instPosMulMono Nat.cast_nonneg'
swap_mem_interedges_iff 📖	mathematical	Symmetric	Finset Finset.instMembership interedges	—	mem_interedges_iff Symmetric.iff

SimpleGraph

Definitions

Name	Category	Theorems
edgeDensity 📖	CompOp	17 math math: edgeDensity_le_one, edgeDensity_def, SzemerediRegularity.le_sum_distinctPairs_edgeDensity_sq, regularityReduced_adj, edgeDensity_empty_right, nonuniformWitnesses_spec, SzemerediRegularity.edgeDensity_chunk_uniform, not_isUniform_iff, Finpartition.coe_energy, edgeDensity_empty_left, nonuniformWitness_spec, Finpartition.mk_mem_sparsePairs, SzemerediRegularity.edgeDensity_chunk_not_uniform, card_interedges_div_card, edgeDensity_add_edgeDensity_compl, edgeDensity_nonneg, edgeDensity_comm
interedges 📖	CompOp	19 math math: edgeDensity_def, interedges_mono, card_interedges_add_card_interedges_compl, interedges_disjoint_left, interedges_empty_left, Finpartition.IsEquipartition.card_interedges_sparsePairs_le, card_interedges_le_mul, interedges_def, mk_mem_interedges_iff, unreduced_edges_subset, interedges_disjoint_right, swap_mem_interedges_iff, mem_interedges_iff, mk_mem_interedges_comm, card_interedges_div_card, interedges_biUnion, interedges_biUnion_left, interedges_biUnion_right, Finpartition.IsEquipartition.card_interedges_sparsePairs_le'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_interedges_add_card_interedges_compl 📖	mathematical	Disjoint Finset Finset.partialOrder Finset.instOrderBot	Finset.card interedges Compl.compl SimpleGraph instCompl Compl.adjDecidable	—	Finset.card_product interedges_def Finset.filter_congr compl_adj Disjoint.forall_ne_finset Finset.mem_product Finset.card_union_of_disjoint Finset.disjoint_filter Finset.filter_union_filter_not_eq
card_interedges_div_card 📖	mathematical	—	Finset.card interedges edgeDensity	—	—
card_interedges_le_mul 📖	mathematical	—	Finset.card interedges	—	Rel.card_interedges_le_mul
edgeDensity_add_edgeDensity_compl 📖	mathematical	Finset.Nonempty Disjoint Finset Finset.partialOrder Finset.instOrderBot	edgeDensity Compl.compl SimpleGraph instCompl Compl.adjDecidable	—	edgeDensity_def add_div div_eq_one_iff_eq ne_of_gt mul_pos IsStrictOrderedRing.toPosMulStrictMono Rat.instIsStrictOrderedRing Nat.cast_pos' Rat.instAddLeftMono Rat.instZeroLEOneClass NeZero.charZero_one Rat.instCharZero Finset.Nonempty.card_pos card_interedges_add_card_interedges_compl
edgeDensity_comm 📖	mathematical	—	edgeDensity	—	Rel.edgeDensity_comm symm
edgeDensity_def 📖	mathematical	—	edgeDensity Finset.card interedges	—	—
edgeDensity_empty_left 📖	mathematical	—	edgeDensity Finset Finset.instEmptyCollection	—	Rel.edgeDensity_empty_left
edgeDensity_empty_right 📖	mathematical	—	edgeDensity Finset Finset.instEmptyCollection	—	Rel.edgeDensity_empty_right
edgeDensity_le_one 📖	mathematical	—	edgeDensity	—	Rel.edgeDensity_le_one
edgeDensity_nonneg 📖	mathematical	—	edgeDensity	—	Rel.edgeDensity_nonneg
interedges_biUnion 📖	mathematical	—	interedges Finset.biUnion SProd.sprod Finset Finset.instSProd	—	Rel.interedges_biUnion
interedges_biUnion_left 📖	mathematical	—	interedges Finset.biUnion	—	Rel.interedges_biUnion_left
interedges_biUnion_right 📖	mathematical	—	interedges Finset.biUnion	—	Rel.interedges_biUnion_right
interedges_def 📖	mathematical	—	interedges Finset.filter Adj SProd.sprod Finset Finset.instSProd	—	—
interedges_disjoint_left 📖	mathematical	Disjoint Finset Finset.partialOrder Finset.instOrderBot	interedges	—	Rel.interedges_disjoint_left
interedges_disjoint_right 📖	mathematical	Disjoint Finset Finset.partialOrder Finset.instOrderBot	interedges	—	Rel.interedges_disjoint_right
interedges_empty_left 📖	mathematical	—	interedges Finset Finset.instEmptyCollection	—	Rel.interedges_empty_left
interedges_mono 📖	mathematical	Finset Finset.instHasSubset	interedges	—	Rel.interedges_mono
mem_interedges_iff 📖	mathematical	—	Finset Finset.instMembership interedges Adj	—	Rel.mem_interedges_iff
mk_mem_interedges_comm 📖	mathematical	—	Finset Finset.instMembership interedges	—	Rel.mk_mem_interedges_comm symm
mk_mem_interedges_iff 📖	mathematical	—	Finset Finset.instMembership interedges Adj	—	Rel.mk_mem_interedges_iff
swap_mem_interedges_iff 📖	mathematical	—	Finset Finset.instMembership interedges	—	Rel.swap_mem_interedges_iff symm

---

← Back to Index