Commit 2023-06-26 08:41 d8a7e7ef

View on Github →

feat: port Combinatorics.SimpleGraph.Regularity.Chunk (#5474)

Estimated changes

Modified Mathlib.lean

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

added theorem SzemerediRegularity.biUnion_star_subset_nonuniformWitness

added theorem SzemerediRegularity.card_biUnion_star_le_m_add_one_card_star_mul

added theorem SzemerediRegularity.card_chunk

added theorem SzemerediRegularity.card_eq_of_mem_parts_chunk

added theorem SzemerediRegularity.card_le_m_add_one_of_mem_chunk_parts

added theorem SzemerediRegularity.edgeDensity_chunk_not_uniform

added theorem SzemerediRegularity.edgeDensity_chunk_uniform

added theorem SzemerediRegularity.m_le_card_of_mem_chunk_parts

added theorem SzemerediRegularity.star_subset_chunk