Removal

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

Statistics

Metric	Count
Definitions evalTriangleRemovalBound, triangleRemovalBound	2
Theorems le_card_cliqueFinset, regularityReduced_edges_card_aux, triangleRemovalBound_le, triangleRemovalBound_mul_cube_lt, triangleRemovalBound_nonpos, triangleRemovalBound_pos, triangle_removal	7
Total	9

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
evalTriangleRemovalBound 📖	CompOp	—

SimpleGraph

Definitions

Name	Category	Theorems
triangleRemovalBound 📖	CompOp	5 math math: triangleRemovalBound_mul_cube_lt, triangleRemovalBound_pos, triangleRemovalBound_le, FarFromTriangleFree.le_card_cliqueFinset, triangleRemovalBound_nonpos

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
regularityReduced_edges_card_aux 📖	mathematical	Real Real.instLT Real.instZero Finpartition.IsEquipartition Finset.univ Finpartition.IsUniform Real.instField Real.linearOrder DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instLE Finset.card Finset Finpartition.parts Finset.instLattice Finset.instOrderBot	Real Real.instLT Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instSub Finset.card Sym2 edgeFinset fintypeEdgeSet Sym2.instFintype regularityReduced Real.instField Real.linearOrder Finset.univ DivInvMonoid.toDiv Real.instDivInvMonoid regularityReduced.instDecidableRel_adj Monoid.toPow Nat.instMonoid Fintype.card	—	Nat.instAtLeastTwoHAddOfNat Finset.univ_product_univ mul_sub Finset.filter_and_not Finset.cast_card_sdiff Finset.monotone_filter_right regularityReduced_le RCLike.charZero_rclike two_mul_card_edgeFinset Nat.mono_cast IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass Finset.card_le_card unreduced_edges_subset Finset.card_union_le add_le_add_left covariant_swap_add_of_covariant_add add_lt_add_left IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le Finpartition.IsEquipartition.sum_nonUniforms_lt Real.instIsStrictOrderedRing Finset.univ_nonempty div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo add_le_add add_le_add_right Finpartition.IsEquipartition.card_biUnion_offDiag_le Finpartition.IsEquipartition.card_interedges_sparsePairs_le le_of_lt Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.isNat_add
triangleRemovalBound_le 📖	mathematical	Real Real.instLE Real.instOne	Real Real.instLE triangleRemovalBound Real.instMul Real.instSub Real.instOne DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Monoid.toPow Real.instMonoid SzemerediRegularity.bound Nat.ceil Real.semiring Real.partialOrder FloorRing.toFloorSemiring Real.instRing Real.linearOrder Real.instIsStrictOrderedRing Real.instFloorRing	—	Nat.instAtLeastTwoHAddOfNat Real.instIsStrictOrderedRing mul_inv_rev inf_of_le_right
triangleRemovalBound_mul_cube_lt 📖	mathematical	Real Real.instLT Real.instZero	Real Real.instLT Real.instMul triangleRemovalBound Monoid.toPow Real.instMonoid Real.instNatCast Nat.ceil Real.semiring Real.partialOrder FloorRing.toFloorSemiring Real.instRing Real.linearOrder Real.instIsStrictOrderedRing Real.instFloorRing DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat Real.instOne	—	Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing min_le_left le_of_lt pow_pos IsStrictOrderedRing.toPosMulStrictMono IsStrictOrderedRing.toZeroLEOneClass Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Mathlib.Meta.Positivity.nat_ceil_pos div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo mul_inv inv_mul_cancel_right₀ ne_of_gt Mathlib.Meta.NormNum.isNNRat_lt_true instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Nat.cast_one
triangleRemovalBound_nonpos 📖	mathematical	Real Real.instLE Real.instZero	Real Real.instLE triangleRemovalBound Real.instZero	—	Real.instIsStrictOrderedRing triangleRemovalBound.eq_1 Nat.ceil_eq_zero div_nonpos_of_nonneg_of_nonpos IsOrderedRing.toPosMulMono Real.instIsOrderedRing CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat MulZeroClass.mul_zero inv_zero
triangleRemovalBound_pos 📖	mathematical	Real Real.instLT Real.instZero	Real Real.instLT Real.instZero triangleRemovalBound	—	Nat.instAtLeastTwoHAddOfNat min_le_left lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_congr Nat.cast_one Mathlib.Tactic.Ring.neg_add 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_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.mul_neg neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Meta.NormNum.isNat_lt_true Real.instIsOrderedRing RCLike.charZero_rclike Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Tactic.CancelDenoms.sub_subst Mathlib.Tactic.CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_nonpos lt_min inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono mul_pos Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial pow_pos IsStrictOrderedRing.toZeroLEOneClass Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instZeroLEOneClass NeZero.charZero_one Mathlib.Meta.Positivity.nat_ceil_pos div_pos SzemerediRegularity.bound_pos
triangle_removal 📖	mathematical	Real Real.instLT Real.instNatCast Finset.card Finset cliqueFinset Real.instMul triangleRemovalBound Monoid.toPow Real.instMonoid Fintype.card	SimpleGraph instLE Adj Real Real.instLT Real.instSub Real.instNatCast Finset.card Sym2 edgeFinset fintypeEdgeSet Sym2.instFintype Real.instMul Monoid.toPow Nat.instMonoid Fintype.card CliqueFree	—	LT.lt.not_ge FarFromTriangleFree.le_card_cliqueFinset farFromTriangleFree_iff le_of_not_gt Mathlib.Tactic.Push.not_and_eq

SimpleGraph.FarFromTriangleFree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_card_cliqueFinset 📖	mathematical	SimpleGraph.FarFromTriangleFree Real Real.instField Real.linearOrder	Real Real.instLE Real.instMul SimpleGraph.triangleRemovalBound Monoid.toPow Real.instMonoid Real.instNatCast Fintype.card Finset.card Finset SimpleGraph.cliqueFinset	—	isEmpty_or_nonempty Fintype.card_eq_zero CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat MulZeroClass.mul_zero Real.instIsOrderedRing le_or_gt LE.le.trans mul_nonpos_of_nonpos_of_nonneg IsOrderedRing.toMulPosMono SimpleGraph.triangleRemovalBound_nonpos le_of_lt pow_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsStrictOrderedRing.toZeroLEOneClass Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one Fintype.card_pos Nat.cast_nonneg' Nat.le_ceil le_total mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono pow_le_pow_left₀ Nat.mono_cast LT.lt.le SimpleGraph.triangleRemovalBound_pos SimpleGraph.triangleRemovalBound_mul_cube_lt LT.lt.ne' Finset.Nonempty.card_pos cliqueFinset_nonempty szemeredi_regularity div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_le SimpleGraph.regularityReduced_edges_card_aux lt_of_mul_lt_mul_left mul_assoc zero_le_two cliqueFinset_nonempty' SimpleGraph.regularityReduced_le lt_one

---

← Back to Index