Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-27 07:01 5ac5c922

View on Github →

feat(combinatorics/simple_graph/regularity/uniform): Witnesses of non-uniformity (#13155) Provide ways to pick witnesses of non-uniformity.

Estimated changes

Modified src/combinatorics/simple_graph/regularity/uniform.lean

modified theorem finpartition.bot_is_uniform

added theorem finpartition.is_uniform.mono

modified theorem finpartition.non_uniforms_bot

added theorem finpartition.non_uniforms_mono

added theorem finpartition.nonuniform_witness_mem_nonuniform_witnesses

added theorem simple_graph.left_nonuniform_witnesses_card

added theorem simple_graph.left_nonuniform_witnesses_subset

added theorem simple_graph.nonuniform_witness_card_le

added theorem simple_graph.nonuniform_witness_spec

added theorem simple_graph.nonuniform_witness_subset

added theorem simple_graph.nonuniform_witnesses_spec

added theorem simple_graph.not_is_uniform_iff

added theorem simple_graph.right_nonuniform_witnesses_card

added theorem simple_graph.right_nonuniform_witnesses_subset