Documentation Verification Report

Lemma

📁 Source: Mathlib/Combinatorics/SimpleGraph/Regularity/Lemma.lean

Statistics

MetricCount
Definitions0
Theoremsszemeredi_regularity
1
Total1

(root)

Theorems

NameKindAssumesProvesValidatesDepends On
szemeredi_regularity 📖mathematicalReal
Real.instLT
Real.instZero
Fintype.card		Finpartition.IsEquipartition
Finset.univ
Finset.card
Finset
Finpartition.parts
Finset.instLattice
Finset.instOrderBot
SzemerediRegularity.bound
Finpartition.IsUniform
Real.instField
Real.linearOrder		—le_total
Finpartition.bot_isEquipartition
Finpartition.card_bot
Finset.card_univ
Finpartition.bot_isUniform
Real.instIsStrictOrderedRing
LE.le.trans
SzemerediRegularity.initialBound_le_bound
Finpartition.exists_equipartition_card_eq
LT.lt.ne'
SzemerediRegularity.initialBound_pos
SzemerediRegularity.le_initialBound
Eq.ge
Eq.le
Finpartition.IsUniform.mono
Finpartition.isUniform_one
Fintype.card_pos_iff
LT.lt.trans_le
SzemerediRegularity.bound_pos
Nat.instAtLeastTwoHAddOfNat
Nat.cast_zero
MulZeroClass.mul_zero
Finpartition.energy_nonneg
Function.iterate_succ_apply'
SzemerediRegularity.le_stepBound
LT.lt.le
SzemerediRegularity.hundred_lt_pow_initialBound_mul
mul_le_mul_of_nonneg_right
IsOrderedRing.toMulPosMono
Real.instIsOrderedRing
pow_right_mono₀
Real.instZeroLEOneClass
IsOrderedRing.toPosMulMono
IsOrderedAddMonoid.toAddLeftMono
Real.instIsOrderedAddMonoid
RCLike.charZero_rclike
le_of_lt
pow_pos
IsStrictOrderedRing.toPosMulStrictMono
IsStrictOrderedRing.toZeroLEOneClass
Nat.cast_one
Finpartition.energy_le_one
le_div_iff₀'
PosMulReflectLE.toPosMulReflectLT
PosMulStrictMono.toPosMulReflectLE
Mathlib.Meta.NormNum.instAtLeastTwo
Mathlib.Meta.NormNum.IsNat.to_eq
Mathlib.Meta.NormNum.isNat_mul
Mathlib.Meta.NormNum.isNat_ofNat
div_le_iff₀
MulPosReflectLE.toMulPosReflectLT
MulPosStrictMono.toMulPosReflectLE
IsStrictOrderedRing.toMulPosStrictMono
Real.instNontrivial
div_mul_eq_mul_div
Function.monotone_iterate_of_id_le
Nat.le_floor
IsStrictOrderedRing.toIsOrderedRing
Nat.instIsStrictOrderedRing
Nat.instNontrivial
SzemerediRegularity.increment_isEquipartition
SzemerediRegularity.card_increment
SzemerediRegularity.stepBound_mono
le_trans
Nat.cast_succ
mul_add
Distrib.leftDistribClass
mul_one
add_le_add_left
covariant_swap_add_of_covariant_add
SzemerediRegularity.energy_increment
SzemerediRegularity.seven_le_initialBound
SzemerediRegularity.stepBound.eq_1
SzemerediRegularity.bound.eq_1
mul_le_mul_right
Nat.instMulLeftMono
pow_le_pow_left'
covariant_swap_mul_of_covariant_mul
lt_irrefl
mul_comm
div_mul_div_cancel₀
div_self
mul_lt_mul_of_pos_left
Nat.lt_floor_add_one
div_pos
Mathlib.Meta.Positivity.pos_of_isNat
Nat.cast_add_one

---

← Back to Index