Commit 2023-03-01 18:09 49583927

View on Github →

feat: Port/Combinatorics.SimpleGraph.Regularity.Uniform (#2547)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean

added theorem Finpartition.IsUniform.mono

added def Finpartition.IsUniform

added theorem Finpartition.botIsUniform

added theorem Finpartition.isUniformOfEmpty

added theorem Finpartition.isUniformOne

added theorem Finpartition.mk_mem_nonUniforms_iff

added theorem Finpartition.nonUniforms_bot

added theorem Finpartition.nonUniforms_mono

added theorem Finpartition.nonempty_of_not_uniform

added theorem Finpartition.nonuniformWitness_mem_nonuniformWitnesses

added theorem SimpleGraph.IsUniform.mono

added theorem SimpleGraph.IsUniform.symm

added def SimpleGraph.IsUniform

added theorem SimpleGraph.isUniform_comm

added theorem SimpleGraph.isUniform_one

added theorem SimpleGraph.isUniform_singleton

added theorem SimpleGraph.left_nonuniformWitnesses_card

added theorem SimpleGraph.left_nonuniformWitnesses_subset

added theorem SimpleGraph.nonuniformWitness_card_le

added theorem SimpleGraph.nonuniformWitness_spec

added theorem SimpleGraph.nonuniformWitness_subset

added theorem SimpleGraph.nonuniformWitnesses_spec

added theorem SimpleGraph.not_isUniform_iff

added theorem SimpleGraph.not_isUniform_zero

added theorem SimpleGraph.right_nonuniformWitnesses_card

added theorem SimpleGraph.right_nonuniformWitnesses_subset