Documentation Verification Report

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.instMul` `Real.instSub` `Sym2` `edgeFinset` `fintypeEdgeSet` `Sym2.instFintype` `regularityReduced` `regularityReduced.instDecidableRel_adj` `Monoid.toNatPow` `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` `AddRightCancelSemigroup.toIsRightCancelAdd` `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`	`triangleRemovalBound` `Real.instMul` `Real.instSub` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Monoid.toNatPow` `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.instMul` `triangleRemovalBound` `Monoid.toNatPow` `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`	`triangleRemovalBound`	—	`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`	`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` `CancelDenoms.sub_subst` `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.toNatPow` `Real.instMonoid` `Fintype.card`	`SimpleGraph` `instLE` `Real.instSub` `Sym2` `edgeFinset` `fintypeEdgeSet` `Sym2.instFintype` `Nat.instMonoid` `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.instLE` `Real.instMul` `SimpleGraph.triangleRemovalBound` `Monoid.toNatPow` `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