Combinatorics.Line.ColorFocused.is_focused
theorem Combinatorics.Line.ColorFocused.is_focused :
∀ {α : Type u_1} {ι : Type u_2} {κ : Type u_3} {C : (ι → Option α) → κ} (self : Combinatorics.Line.ColorFocused C),
∀ p ∈ self.lines, (fun x i => (p.line.idxFun i).getD x) none = self.focus
This theorem states that in a color-focused collection of lines, all lines have the same endpoint, or focus. More specifically, given a function `C` that maps a line to a color and a `ColorFocused` instance `self` based on `C`, for each line `p` in the collection described by `self`, the endpoint of `p` when viewed as a function (given by `p.line.idxFun`) applied to the color `none`, is equal to the `focus` of the `ColorFocused` instance. The types `α`, `ι`, and `κ` are arbitrary, allowing this theorem to apply to a wide range of color-focused collections.
More concisely: For any color-focused collection `self` and function `C` mapping lines to colors, the endpoint of each line in `self` when applied to color `none` equals the focus of the collection.
|
Combinatorics.Line.proper
theorem Combinatorics.Line.proper :
∀ {α : Type u_1} {ι : Type u_2} (self : Combinatorics.Line α ι), ∃ i, self.idxFun i = none
This theorem states that for every line in the combinatorics context (represented as `Combinatorics.Line`), there exists at least one coordinate `i` for which the `idxFun` applied to `i` equals `none`. In other words, the function that maps an element `x` to `l x i` returns `id` for at least one `i`, which ensures that the combinatorial lines are nontrivial. This requirement is a fundamental property of combinatorial lines.
More concisely: For every combinatorics line, there exists an index i such that the function mapping an element to the line's i-th coordinate evaluates to none.
|
Combinatorics.Line.ColorFocused.distinct_colors
theorem Combinatorics.Line.ColorFocused.distinct_colors :
∀ {α : Type u_1} {ι : Type u_2} {κ : Type u_3} {C : (ι → Option α) → κ} (self : Combinatorics.Line.ColorFocused C),
(Multiset.map Combinatorics.Line.AlmostMono.color self.lines).Nodup
This theorem states that in a color-focused collection of lines, all lines have distinct colors. Specifically, given a function `C` that maps a function from `ι` to `Option α` to some color `κ`, and a color-focused collection of lines `self`, it asserts that when you map each line in the collection to its main color using `Combinatorics.Line.AlmostMono.color` and collect the results into a multiset, there are no duplicate colors in the multiset. This corresponds to the mathematical statement that the colors of the lines in a color-focused collection are all distinct.
More concisely: In a color-focused collection of lines, all lines have distinct colors. That is, the multiset of main colors of lines in a color-focused collection is empty of repetitions.
|
Combinatorics.Line.exists_mono_in_high_dimension
theorem Combinatorics.Line.exists_mono_in_high_dimension :
∀ (α : Type u) [inst : Finite α] (κ : Type v) [inst : Finite κ],
∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, Combinatorics.Line.IsMono C l
The Hales-Jewett theorem states that for any finite types `α` and `κ`, there exists a finite type `ι` such that whenever we color the hypercube `ι → α` with `κ` colors, there will always be a monochromatic combinatorial line. A line is monochromatic if all its points are of the same color. Here, the color of a point is determined by the function `C : (ι → α) → κ`. In other words, no matter how you color the points of a high-dimensional cube, there's always a straight line that's all one color.
More concisely: Given any finite types `α` and `κ`, there exists a finite type `ι` such that every coloring of the `ι → α` hypercube with `κ` colors contains a monochromatic line.
|
Combinatorics.exists_mono_homothetic_copy
theorem Combinatorics.exists_mono_homothetic_copy :
∀ {M : Type u_1} {κ : Type u_2} [inst : AddCommMonoid M] (S : Finset M) [inst_1 : Finite κ] (C : M → κ),
∃ a > 0, ∃ b c, ∀ s ∈ S, C (a • s + b) = c
The theorem `Combinatorics.exists_mono_homothetic_copy` is a generalization of Van der Waerden's theorem. It states that for any given type `M` representing an additively commutative monoid and a finite set `S` of this type, and any finite coloring `C` (a function that assigns a color, represented by the type κ, to each element of `M`), there exists a positive integer `a`, and elements `b` and `c` such that every element `s` in the set `S`, when scaled by `a` and translated by `b` (forming `a • s + b`), is assigned the same color `c` by the coloring `C`. That is to say, there is a monochromatic (single-color) homothetic (uniformly scaled and translated) copy of the set `S`.
More concisely: Given an additively commutative monoid M, a finite coloring C of M with finitely many colors, there exists an integer a > 0 and elements b and c in M such that for all s in the finite set S, the scaled and translated elements a * s + b have the same color c under the coloring C.
|
Combinatorics.Line.AlmostMono.has_color
theorem Combinatorics.Line.AlmostMono.has_color :
∀ {α : Type u_1} {ι : Type u_2} {κ : Type u_3} {C : (ι → Option α) → κ} (self : Combinatorics.Line.AlmostMono C)
(x : α), C ((fun x i => (self.line.idxFun i).getD x) (some x)) = self.color
This theorem states that for an almost monochromatic line (a line where all points are of the same color except possibly the endpoints), the color of the line at any given point is equal to the main color of the line. This is true for all types of elements `α`, index sets `ι`, colorings `κ`, and given an almost monochromatic line `self` and an element `x` of type `α`. The color of the line at a given point is determined by the function `C` applied to the function that, for a given index `i`, returns the color at that index. The main color of the line is indicated by `self.color`.
More concisely: For any almost monochromatic line `self` and element `x` of type `α`, the color of `x` on the line `self` equals the main color `self.color`.
|