RelSeries.smash.proof_2
theorem RelSeries.smash.proof_2 :
∀ {α : Type u_1} {r : Rel α α} (p q : RelSeries r) (i : Fin (p.length + q.length + 1)),
¬↑i < p.length → ↑i - p.length < q.length + 1
This theorem states that for any type `α` and any relation `r` on `α`, given two series of relations `p` and `q` and a finite index `i` that is less than the sum of the lengths of `p` and `q` plus one, if it is not the case that the value of `i` is less than the length of `p`, then the value of `i` subtracted by the length of `p` is less than the length of `q` plus one. This theorem is about manipulating the indices involved in 'smashing' together two series of relations.
More concisely: For any type `α` and relation `r` on `α`, if index `i` is not less than the length of `p` in a series of relations `p` and `q`, then `i - length(p) < length(q) + 1`.
|
LTSeries.strictMono
theorem LTSeries.strictMono : ∀ {α : Type u_1} [inst : Preorder α] (x : LTSeries α), StrictMono x.toFun
The theorem `LTSeries.strictMono` states that for any type `α` that has a preorder structure, if `x` is a `LTSeries` over `α`, then the function associated with `x` (accessed by `x.toFun`) is strictly monotonic. In other words, for any two elements `a` and `b` in `α` such that `a < b`, the value of the function at `a` is strictly less than the value of the function at `b`.
More concisely: For any preordered type `α` and `LTSeries` `x` over `α`, the function `x.toFun` is strictly monotonic: `x.toFun a < x.toFun b` for all `a, b ∈ α` with `a < b`.
|
LTSeries.nonempty_of_infiniteDimensionalType
theorem LTSeries.nonempty_of_infiniteDimensionalType :
∀ (α : Type u_1) [inst : Preorder α] [inst : InfiniteDimensionalOrder α], Nonempty α
This theorem states that if a type `α` is infinite dimensional, then `α` is nonempty. In the context of this theorem, a type is considered infinite dimensional if it has a `LTSeries` of arbitrary length. Here, `LTSeries` likely refers to a series of elements of the type `α` such that each element is less than the next. The 'Preorder' structure on `α` ensures that the "<" comparison is well-defined.
More concisely: If a type `α` has an infinite LTSeries, then `α` is nonempty.
|
RelSeries.nonempty_of_infiniteDimensional
theorem RelSeries.nonempty_of_infiniteDimensional :
∀ {α : Type u_1} (r : Rel α α) [inst : r.InfiniteDimensional], Nonempty α
This theorem states that if a relation `r`, defined on a type `α`, is infinite dimensional, then the type `α` is nonempty. In other words, if we have a relation that can be represented in an infinite dimensional space, there must exist at least one element in the set `α`. This is because an empty set cannot form a relation that is infinite dimensional.
More concisely: If a relation on a type is infinite-dimensional, then the type is nonempty.
|
Rel.FiniteDimensional.exists_longest_relSeries
theorem Rel.FiniteDimensional.exists_longest_relSeries :
∀ {α : Type u_1} {r : Rel α α} [self : r.FiniteDimensional], ∃ x, ∀ (y : RelSeries r), y.length ≤ x.length := by
sorry
This theorem states that a relation `r` is said to be finite dimensional if and only if there exists a relation series of `r` that has the maximum length. In other words, for every set-valued function `r` on a type `α` that is finite dimensional, there always exists a relation series (a sequence of relations) `x` such that for any other relation series `y`, the length of `y` is less than or equal to the length of `x`. This essentially means that there is a longest relation series in the space of all relation series of the finite dimensional relation `r`.
More concisely: A relation on a type is finite dimensional if and only if there exists a maximal relation series for it.
|
RelSeries.step
theorem RelSeries.step :
∀ {α : Type u_1} {r : Rel α α} (self : RelSeries r) (i : Fin self.length),
r (self.toFun i.castSucc) (self.toFun i.succ)
The theorem `RelSeries.step` states that for any type `α` and a relation `r` on `α`, given a series defined by this relation `r`, any two adjacent elements in this series are related by `r`. More specifically, if `i` is an element in the finite domain of the series, then the `i`-th element and the (i+1)-th element in the series (obtained by applying the series function `toFun` to `i.castSucc` and `i.succ` respectively) are related by `r`.
More concisely: For any series defined by a relation `r` on a type `α`, the `i`-th and `(i+1)`-th elements in the series are related by `r`.
|
Rel.InfiniteDimensional.exists_relSeries_with_length
theorem Rel.InfiniteDimensional.exists_relSeries_with_length :
∀ {α : Type u_1} {r : Rel α α} [self : r.InfiniteDimensional] (n : ℕ), ∃ x, x.length = n
This theorem states that for any relation `r` on a type `α`, if `r` is infinite dimensional (which means there exist relation series of arbitrary length), then for any natural number `n`, there exists a relation series `x` such that the length of `x` is equal to `n`. In other words, we can find a relation series of any given length in an infinite dimensional relation.
More concisely: In an infinite-dimensional relation, there exists a relation series of length any given natural number.
|