Commit 2023-02-21 09:26 f2e18b20

View on Github →

feat: port Combinatorics.HalesJewett (#1704)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/HalesJewett.lean

added structure Combinatorics.Line.AlmostMono

added structure Combinatorics.Line.ColorFocused

added def Combinatorics.Line.IsMono

added theorem Combinatorics.Line.apply

added theorem Combinatorics.Line.apply_none

added theorem Combinatorics.Line.apply_of_ne_none

added def Combinatorics.Line.diagonal

added theorem Combinatorics.Line.diagonal_apply

added theorem Combinatorics.Line.exists_mono_in_high_dimension

added def Combinatorics.Line.horizontal

added theorem Combinatorics.Line.horizontal_apply

added def Combinatorics.Line.map

added theorem Combinatorics.Line.map_apply

added def Combinatorics.Line.prod

added theorem Combinatorics.Line.prod_apply

added def Combinatorics.Line.vertical

added theorem Combinatorics.Line.vertical_apply

added structure Combinatorics.Line

added theorem Combinatorics.exists_mono_homothetic_copy