Counting

📁 Source: Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean

Statistics

Metric	Count
Definitions	0
Theorems triangle_counting, triangle_counting'	2
Total	2

SimpleGraph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
triangle_counting 📖	mathematical	Real Real.instLE Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instRatCast edgeDensity IsUniform Real.instField Real.linearOrder Disjoint Finset Finset.partialOrder Finset.instOrderBot	Real Real.instLE Real.instMul Real.instSub Real.instOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Monoid.toPow Real.instMonoid Finset.card Finset cliqueFinset	—	Nat.instAtLeastTwoHAddOfNat LE.le.trans triangle_counting' Nat.cast_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Finset.card_le_card_of_injOn Finset.coe_filter coe_cliqueFinset
triangle_counting' 📖	mathematical	Real Real.instLE Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instRatCast edgeDensity IsUniform Real.instField Real.linearOrder	Real Real.instLE Real.instMul Real.instSub Real.instOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Monoid.toPow Real.instMonoid Finset.card Finset.filter Adj SProd.sprod Finset Finset.instSProd	—	Nat.instAtLeastTwoHAddOfNat le_trans Finset.card_biUnion Function.onFun.eq_1 Finset.disjoint_left Nat.cast_sum nsmul_eq_mul LT.lt.le IsUniform.pos Real.instIsStrictOrderedRing Finset.union_subset Finset.filter_subset sub_mul one_mul Finset.card_sdiff_of_subset Nat.cast_sub Finset.card_le_card sub_le_sub_iff_left IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add mul_assoc mul_comm two_mul LE.le.trans Nat.cast_le Real.instZeroLEOneClass IsStrictOrderedRing.toCharZero Finset.card_union_le Nat.cast_add add_le_add Eq.trans_le Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one 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.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 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.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_gt mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing mul_nonneg IsOrderedRing.toPosMulMono pow_nonneg IsOrderedRing.toZeroLEOneClass Nat.cast_nonneg' Finset.card_nsmul_le_sum

---

← Back to Index