Commit 2024-10-22 13:55 9a0d45fe

View on Github →

chore(Combinatorics): use newly introduced finset notation (#18055) For s : Finset α, replace s.card with #s, s.filter p with {x ∈ s | p x}, ∑ x ∈ s.filter p, f x with ∑ x ∈ s with p x, f x. Rewrap lines around and open the Finset locale where necessary.

Estimated changes

modified theorem Behrend.card_box
modified def Behrend.sphere
modified theorem mulRothNumber_le
modified theorem Finset.card_mul_divConst
modified theorem Finset.card_mul_mulConst
modified theorem Finset.cast_addConst
modified theorem Finset.cast_divConst
modified theorem Finset.cast_mulConst
modified theorem Finset.cast_subConst
modified def Finset.divConst
modified theorem Finset.divConst_mul_card
modified def Finset.mulConst
modified theorem Finset.mulConst_mul_card
modified theorem Int.erdos_ginzburg_ziv
modified theorem ZMod.erdos_ginzburg_ziv
modified def Finset.Colex.initSeg
modified theorem Finset.Colex.mem_initSeg
modified def Finset.bipartiteAbove
modified def Finset.bipartiteBelow
modified theorem Down.card_compression
modified theorem Set.Sized.uvCompression
modified theorem UV.card_compress
modified theorem UV.card_compression
modified theorem UV.compress_injOn
modified theorem Finset.card_le_card_diffs
modified theorem Finset.iterated_kk
modified theorem Finset.kruskal_katona
modified theorem Finset.mem_falling
modified def Finset.shatterer
modified theorem SimpleGraph.isNClique_iff
modified def Rel.edgeDensity
modified def Rel.interedges
modified theorem SimpleGraph.edgeDensity_def
modified theorem SimpleGraph.interedges_def
modified def SimpleGraph.degree
modified theorem SimpleGraph.edgeFinset_card
modified theorem SzemerediRegularity.eps_pos
modified theorem SzemerediRegularity.m_pos