Commit 2022-10-18 04:47 8f774b71

View on Github →

feat(combinatorics/simple_graph/regularity/bound): positivity extension (#16639) Add a positivity extension for szemeredi_regularity.initial_bound and szemeredi_regularity.bound.

Estimated changes

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

deleted theorem szemeredi_regularity.four_pow_pos

modified theorem szemeredi_regularity.step_bound_pos_iff