Documentation Verification Report

Uniform

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

Statistics

Metric	Count
Definitions `IsUniform`, `nonUniforms`, `nonuniformWitnesses`, `sparsePairs`, `IsUniform`, `instDecidableRel`, `nonuniformWitness`, `nonuniformWitnesses`, `regularityReduced`, `instDecidableRel_adj`	10
Theorems `card_biUnion_offDiag_le`, `card_biUnion_offDiag_le'`, `card_interedges_sparsePairs_le`, `card_interedges_sparsePairs_le'`, `sum_nonUniforms_lt`, `sum_nonUniforms_lt'`, `mono`, `bot_isUniform`, `card_nonuniformWitnesses_le`, `isUniformOfEmpty`, `isUniform_one`, `mk_mem_nonUniforms`, `mk_mem_sparsePairs`, `nonUniforms_bot`, `nonUniforms_mono`, `nonempty_of_not_uniform`, `nonuniformWitness_mem_nonuniformWitnesses`, `sparsePairs_mono`, `mono`, `pos`, `isUniform_comm`, `isUniform_one`, `isUniform_singleton`, `le_card_nonuniformWitness`, `left_nonuniformWitnesses_card`, `left_nonuniformWitnesses_subset`, `nonuniformWitness_spec`, `nonuniformWitness_subset`, `nonuniformWitnesses_spec`, `not_isUniform_iff`, `not_isUniform_zero`, `regularityReduced_adj`, `regularityReduced_anti`, `regularityReduced_le`, `regularityReduced_mono`, `right_nonuniformWitnesses_card`, `right_nonuniformWitnesses_subset`, `unreduced_edges_subset`	38
Total	48

Finpartition

Definitions

Name	Category	Theorems
`IsUniform` 📖	MathDef	4 math math: `isUniformOfEmpty`, `bot_isUniform`, `isUniform_one`, `szemeredi_regularity`
`nonUniforms` 📖	CompOp	6 math math: `nonUniforms_mono`, `mk_mem_nonUniforms`, `IsEquipartition.sum_nonUniforms_lt'`, `SimpleGraph.unreduced_edges_subset`, `IsEquipartition.sum_nonUniforms_lt`, `nonUniforms_bot`
`nonuniformWitnesses` 📖	CompOp	2 math math: `card_nonuniformWitnesses_le`, `nonuniformWitness_mem_nonuniformWitnesses`
`sparsePairs` 📖	CompOp	5 math math: `IsEquipartition.card_interedges_sparsePairs_le`, `SimpleGraph.unreduced_edges_subset`, `sparsePairs_mono`, `mk_mem_sparsePairs`, `IsEquipartition.card_interedges_sparsePairs_le'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_isUniform` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	`IsUniform` `Bot.bot` `Finpartition` `Finset` `Finset.instLattice` `Finset.instOrderBot` `instBotFinset`	—	`IsUniform.eq_1` `card_bot` `nonUniforms_bot` `Finset.card_empty` `Nat.cast_zero` `mul_nonneg` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `Nat.cast_nonneg` `LT.lt.le`
`card_nonuniformWitnesses_le` 📖	mathematical	—	`Finset.card` `Finset` `nonuniformWitnesses` `Finset.filter` `SimpleGraph.IsUniform` `Finset.decidableEq` `SimpleGraph.IsUniform.instDecidableRel` `parts` `Finset.instLattice` `Finset.instOrderBot`	—	`Finset.card_image_le`
`isUniformOfEmpty` 📖	mathematical	`parts` `Finset` `Finset.instLattice` `Finset.instOrderBot` `Finset.instEmptyCollection`	`IsUniform`	—	`Finset.filter.congr_simp` `Finset.filter_empty` `Nat.cast_zero` `zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul`
`isUniform_one` 📖	mathematical	—	`IsUniform` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	—	`IsUniform.eq_1` `mul_one` `Nat.cast_le` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `LE.le.trans` `Finset.card_filter_le` `Finset.offDiag_card` `le_refl`
`mk_mem_nonUniforms` 📖	mathematical	—	`Finset` `Finset.instMembership` `nonUniforms` `parts` `Finset.instLattice` `Finset.instOrderBot` `SimpleGraph.IsUniform`	—	`nonUniforms.eq_1` `Finset.mem_filter` `Finset.mem_offDiag`
`mk_mem_sparsePairs` 📖	mathematical	—	`Finset` `Finset.instMembership` `sparsePairs` `parts` `Finset.instLattice` `Finset.instOrderBot` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivisionRing.toRatCast` `Field.toDivisionRing` `SimpleGraph.edgeDensity`	—	`sparsePairs.eq_1` `Finset.mem_filter` `Finset.mem_offDiag`
`nonUniforms_bot` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	`nonUniforms` `Bot.bot` `Finpartition` `Finset` `Finset.instLattice` `Finset.instOrderBot` `instBotFinset` `Finset.instEmptyCollection`	—	`Finset.eq_empty_iff_forall_notMem` `Finset.singleton_injective` `SimpleGraph.isUniform_singleton`
`nonUniforms_mono` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Finset` `Finset.instHasSubset` `nonUniforms`	—	`Finset.monotone_filter_right` `SimpleGraph.IsUniform.mono`
`nonempty_of_not_uniform` 📖	mathematical	`IsUniform`	`Finset.Nonempty` `Finset` `parts` `Finset.instLattice` `Finset.instOrderBot`	—	`Finset.nonempty_of_ne_empty` `isUniformOfEmpty`
`nonuniformWitness_mem_nonuniformWitnesses` 📖	mathematical	`SimpleGraph.IsUniform` `Finset` `Finset.instMembership` `parts` `Finset.instLattice` `Finset.instOrderBot`	`nonuniformWitnesses` `SimpleGraph.nonuniformWitness`	—	`Finset.mem_image_of_mem` `Finset.mem_filter`
`sparsePairs_mono` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Finset` `Finset.instHasSubset` `sparsePairs`	—	`Finset.monotone_filter_right` `LE.le.trans_lt'`

Finpartition.IsEquipartition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_biUnion_offDiag_le` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Finpartition.IsEquipartition` `Preorder.toLE` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Nat.instAtLeastTwoHAddOfNat` `Finset.card` `Finset` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot`	`Finset.biUnion` `Finset.offDiag` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`Nat.instAtLeastTwoHAddOfNat` `Finset.eq_empty_or_nonempty` `Unique.instSubsingleton` `Nat.cast_zero` `zero_pow` `Nat.instCharZero` `MulZeroClass.mul_zero` `LE.le.trans` `card_biUnion_offDiag_le'` `div_le_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Nat.cast_pos` `IsStrictOrderedRing.toIsOrderedRing` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Finset.Nonempty.card_pos` `Finpartition.parts_nonempty` `Finset.Nonempty.ne_empty` `two_mul` `add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `Nat.mono_cast` `IsStrictOrderedRing.toZeroLEOneClass` `Finpartition.card_parts_le_card` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `le_of_lt` `Nat.cast_pos'` `NeZero.charZero_one` `div_le_iff₀'` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `div_pos` `Mathlib.Meta.Positivity.pos_of_isNat` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `one_div_div` `mul_left_comm` `sq` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `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.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Nat.cast_one` `Mathlib.Tactic.Ring.div_congr` `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.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `mul_nonneg` `zero_le_two` `sq_nonneg` `AddGroup.existsAddOfLE`
`card_biUnion_offDiag_le'` 📖	mathematical	`Finpartition.IsEquipartition`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Finset.card` `Finset.biUnion` `Finset` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot` `Finset.offDiag` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Distrib.toAdd`	—	`Finset.eq_empty_or_nonempty` `Nat.cast_zero` `add_zero` `div_zero` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `Finset.card_biUnion_le_card_mul` `card_part_le_average_add_one` `LE.le.trans` `Finset.offDiag_card` `one_mul` `mul_assoc` `mul_le_mul` `IsOrderedRing.toPosMulMono` `IsOrderedRing.toMulPosMono` `Nat.cast_add` `Nat.cast_one` `covariant_swap_add_of_covariant_add` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Nat.cast_div_le` `le_of_lt` `Nat.cast_pos'` `NeZero.charZero_one` `Right.add_pos_of_nonneg_of_pos` `Nat.instIsOrderedAddMonoid` `zero_le` `Nat.instCanonicallyOrderedAdd` `Mathlib.Meta.Positivity.pos_of_isNat` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_nonneg'` `div_add_same` `LT.lt.ne'` `Finset.Nonempty.card_pos` `mul_div_assoc`
`card_interedges_sparsePairs_le` 📖	mathematical	`Finpartition.IsEquipartition` `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`	`AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Finset.card` `Finset.biUnion` `Finset` `Finpartition.sparsePairs` `SimpleGraph.interedges` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`Nat.instAtLeastTwoHAddOfNat` `card_interedges_sparsePairs_le'` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `pow_le_pow_left₀` `IsOrderedRing.toMulPosMono` `add_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `Nat.cast_nonneg'` `IsStrictOrderedRing.toZeroLEOneClass` `add_le_add_right` `Nat.mono_cast` `Finpartition.card_parts_le_card` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `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.mul_pf_right` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.one_pow`
`card_interedges_sparsePairs_le'` 📖	mathematical	`Finpartition.IsEquipartition` `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`	`AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Finset.card` `Finset.biUnion` `Finset` `Finpartition.sparsePairs` `SimpleGraph.interedges` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Distrib.toAdd` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot`	—	`IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `Finset.card_biUnion_le` `Finset.sum_le_sum` `LT.lt.le` `div_lt_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Nat.cast_pos` `instNontrivialOfCharZero` `Finset.Nonempty.card_pos` `Finpartition.nonempty_of_mem_parts` `Rat.cast_div` `Rat.cast_natCast` `Rat.cast_mul` `Finset.sum_le_sum_of_subset_of_nonneg` `Finset.filter_subset` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Nat.cast_nonneg'` `Finset.mul_sum` `Finset.sum_congr` `mul_le_mul_of_nonneg_left` `Nat.mono_cast` `Finset.sum_le_card_nsmul` `Nat.instIsOrderedAddMonoid` `sq` `card_part_le_average_add_one` `smul_eq_mul` `Finset.offDiag_card` `mul_pow` `mul_add_one` `Distrib.leftDistribClass` `pow_le_pow_left₀` `Nat.instIsStrictOrderedRing` `IsOrderedRing.toMulPosMono` `add_nonneg` `zero_le` `Nat.instCanonicallyOrderedAdd` `add_le_add_left` `covariant_swap_add_of_covariant_add`
`sum_nonUniforms_lt` 📖	mathematical	`Finset.Nonempty` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Finpartition.IsEquipartition` `Finpartition.IsUniform`	`AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Finset.card` `Finset.biUnion` `Finset` `Finpartition.nonUniforms` `SProd.sprod` `Finset.instSProd` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`Nat.instAtLeastTwoHAddOfNat` `Finset.sum_congr` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `Finset.card_biUnion_le` `sum_nonUniforms_lt'` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `pow_le_pow_left₀` `IsOrderedRing.toMulPosMono` `le_of_lt` `add_pos_of_pos_of_nonneg` `Nat.cast_pos'` `NeZero.charZero_one` `Finset.Nonempty.card_pos` `Nat.cast_nonneg'` `add_le_add_right` `Nat.mono_cast` `Finpartition.card_parts_le_card` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `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.mul_pf_right` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.one_pow`
`sum_nonUniforms_lt'` 📖	mathematical	`Finset.Nonempty` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Finpartition.IsEquipartition` `Finpartition.IsUniform`	`Finset.sum` `Finset` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finpartition.nonUniforms` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Finset.card` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Distrib.toAdd` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot`	—	`Finset.sum_le_card_nsmul` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `sq` `Nat.cast_mul` `Nat.cast_le` `IsStrictOrderedRing.toZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `card_part_le_average_add_one` `nsmul_eq_mul` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `le_of_lt` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Nat.cast_pos'` `NeZero.charZero_one` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `Nat.instIsOrderedAddMonoid` `zero_le` `Nat.instCanonicallyOrderedAdd` `Mathlib.Meta.Positivity.pos_of_isNat` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `mul_right_comm` `mul_comm` `mul_lt_mul_of_pos_right` `IsStrictOrderedRing.toMulPosStrictMono` `Finset.Nonempty.card_pos` `Finpartition.parts_nonempty` `Finset.Nonempty.ne_empty`

Finpartition.IsUniform

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mono` 📖	—	`Finpartition.IsUniform` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	—	`LE.le.trans` `Nat.cast_le` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `Finset.card_le_card` `Finpartition.nonUniforms_mono` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Nat.cast_nonneg'`

SimpleGraph

Definitions

Name	Category	Theorems
`IsUniform` 📖	MathDef	10 math math: `SzemerediRegularity.le_sum_distinctPairs_edgeDensity_sq`, `regularityReduced_adj`, `Finpartition.mk_mem_nonUniforms`, `isUniform_one`, `isUniform_singleton`, `Finpartition.card_nonuniformWitnesses_le`, `not_isUniform_iff`, `isUniform_comm`, `IsUniform.symm`, `not_isUniform_zero`
`nonuniformWitness` 📖	CompOp	5 math math: `SzemerediRegularity.biUnion_star_subset_nonuniformWitness`, `Finpartition.nonuniformWitness_mem_nonuniformWitnesses`, `le_card_nonuniformWitness`, `nonuniformWitness_spec`, `nonuniformWitness_subset`
`nonuniformWitnesses` 📖	CompOp	5 math math: `nonuniformWitnesses_spec`, `right_nonuniformWitnesses_subset`, `right_nonuniformWitnesses_card`, `left_nonuniformWitnesses_card`, `left_nonuniformWitnesses_subset`
`regularityReduced` 📖	CompOp	6 math math: `regularityReduced_adj`, `regularityReduced_mono`, `unreduced_edges_subset`, `regularityReduced_le`, `regularityReduced_anti`, `regularityReduced_edges_card_aux`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isUniform_comm` 📖	mathematical	—	`IsUniform`	—	`IsUniform.symm`
`isUniform_one` 📖	mathematical	—	`IsUniform` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	—	`Finset.eq_of_subset_of_card_le` `Nat.cast_le` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `mul_one` `sub_self` `abs_zero` `zero_lt_one` `NeZero.charZero_one`
`isUniform_singleton` 📖	mathematical	—	`IsUniform` `Finset` `Finset.instSingleton` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`IsUniform.pos` `Finset.subset_singleton_iff` `Nat.cast_zero` `LT.lt.not_ge` `one_mul` `Nat.cast_one` `Finset.card_singleton` `sub_self` `abs_zero` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing`
`le_card_nonuniformWitness` 📖	mathematical	`IsUniform`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Finset.card` `nonuniformWitness`	—	`left_nonuniformWitnesses_card` `right_nonuniformWitnesses_card` `IsUniform.symm`
`left_nonuniformWitnesses_card` 📖	mathematical	`IsUniform`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Finset.card` `Finset` `nonuniformWitnesses`	—	`nonuniformWitnesses.eq_1` `not_isUniform_iff`
`left_nonuniformWitnesses_subset` 📖	mathematical	`IsUniform`	`Finset` `Finset.instHasSubset` `nonuniformWitnesses`	—	`nonuniformWitnesses.eq_1` `not_isUniform_iff`
`nonuniformWitness_spec` 📖	mathematical	`IsUniform`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivisionRing.toRatCast` `Field.toDivisionRing` `abs` `Rat.instLattice` `Rat.addGroup` `edgeDensity` `nonuniformWitness`	—	`trichotomous_of` `IsWellOrder.toTrichotomous` `WellOrderingRel.isWellOrder` `asymm` `instAsymmOfIsWellFounded` `IsWellOrder.toIsWellFounded` `nonuniformWitnesses_spec` `edgeDensity_comm` `IsUniform.symm`
`nonuniformWitness_subset` 📖	mathematical	`IsUniform`	`Finset` `Finset.instHasSubset` `nonuniformWitness`	—	`left_nonuniformWitnesses_subset` `right_nonuniformWitnesses_subset` `IsUniform.symm`
`nonuniformWitnesses_spec` 📖	mathematical	`IsUniform`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivisionRing.toRatCast` `Field.toDivisionRing` `abs` `Rat.instLattice` `Rat.addGroup` `edgeDensity` `Finset` `nonuniformWitnesses`	—	`nonuniformWitnesses.eq_1` `not_isUniform_iff`
`not_isUniform_iff` 📖	mathematical	—	`IsUniform` `Finset` `Finset.instHasSubset` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Finset.card` `DivisionRing.toRatCast` `abs` `Rat.instLattice` `Rat.addGroup` `edgeDensity`	—	`Rat.cast_abs` `Rat.cast_sub` `IsStrictOrderedRing.toCharZero`
`not_isUniform_zero` 📖	mathematical	—	`IsUniform` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`LE.le.not_gt` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `covariant_swap_add_of_covariant_add` `Finset.empty_subset` `MulZeroClass.mul_zero` `Nat.cast_zero`
`regularityReduced_adj` 📖	mathematical	—	`Adj` `regularityReduced` `Finset` `Finset.instMembership` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot` `IsUniform` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivisionRing.toRatCast` `Field.toDivisionRing` `edgeDensity`	—	—
`regularityReduced_anti` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`SimpleGraph` `instLE` `regularityReduced`	—	`LE.le.trans`
`regularityReduced_le` 📖	mathematical	—	`SimpleGraph` `instLE` `regularityReduced`	—	—
`regularityReduced_mono` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`SimpleGraph` `instLE` `regularityReduced`	—	`IsUniform.mono`
`right_nonuniformWitnesses_card` 📖	mathematical	`IsUniform`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Finset.card` `Finset` `nonuniformWitnesses`	—	`nonuniformWitnesses.eq_1` `not_isUniform_iff`
`right_nonuniformWitnesses_subset` 📖	mathematical	`IsUniform`	`Finset` `Finset.instHasSubset` `nonuniformWitnesses`	—	`nonuniformWitnesses.eq_1` `not_isUniform_iff`
`unreduced_edges_subset` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `Finset.filter` `Adj` `regularityReduced` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Nat.instAtLeastTwoHAddOfNat` `regularityReduced.instDecidableRel_adj` `SProd.sprod` `Finset.instSProd` `Finset.instUnion` `Finset.biUnion` `Finpartition.nonUniforms` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot` `Finset.offDiag` `Finpartition.sparsePairs` `interedges`	—	`Nat.instAtLeastTwoHAddOfNat` `Finset.filter.congr_simp` `Finpartition.mk_mem_nonUniforms` `Finpartition.exists_mem` `eq_or_ne` `ne_of_adj`

SimpleGraph.IsUniform

Definitions

Name	Category	Theorems
`instDecidableRel` 📖	CompOp	2 math math: `SzemerediRegularity.le_sum_distinctPairs_edgeDensity_sq`, `Finpartition.card_nonuniformWitnesses_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mono` 📖	—	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SimpleGraph.IsUniform`	—	—	`LT.lt.trans_le` `le_trans` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toZeroLEOneClass`
`pos` 📖	mathematical	`SimpleGraph.IsUniform`	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`not_le` `LE.le.not_gt` `LE.le.trans` `abs_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `covariant_swap_add_of_covariant_add` `Finset.empty_subset` `Nat.cast_zero` `mul_nonpos_of_nonneg_of_nonpos` `IsOrderedRing.toPosMulMono` `Nat.cast_nonneg`

SimpleGraph.regularityReduced

Definitions

Name	Category	Theorems
`instDecidableRel_adj` 📖	CompOp	2 math math: `SimpleGraph.unreduced_edges_subset`, `SimpleGraph.regularityReduced_edges_card_aux`

---

← Back to Index