ComplexShape.prev_eq
theorem ComplexShape.prev_eq :
∀ {ι : Type u_1} (self : ComplexShape ι) {i i' j : ι}, self.Rel i j → self.Rel i' j → i = i'
This theorem states that for any type `ι`, and any `ComplexShape` of `ι`, and any three elements of type `ι`, denoted as `i`, `i'`, and `j`, if the relationship `Rel` holds between `i` and `j`, and also between `i'` and `j`, then `i` must be equal to `i'`. In other words, there can be at most one unique nonzero differential to a given element `j` of the `ComplexShape`. This is a uniqueness property related to the structure of the `ComplexShape`.
More concisely: If `ι` is a type, `ComplexShape` is a `ι`-shaped complex, and `i`, `i'` are elements of `ι` such that `Rel` holds between `i` and `j` as well as between `i'` and `j` for some `j`, then `i` equals `i'`. (Uniqueness property: there is at most one nonzero differential to a given element of a `ComplexShape`.)
|
ComplexShape.prev_eq'
theorem ComplexShape.prev_eq' : ∀ {ι : Type u_1} (c : ComplexShape ι) {i j : ι}, c.Rel i j → c.prev j = i
This theorem states that for any type `ι`, and for any `ComplexShape` `c` on `ι`, if there is a relation `Rel` from `i` to `j` in `ComplexShape` `c`, then the `prev` function of `ComplexShape` `c` applied to `j` is equal to `i`. In essence, it establishes that if a relation between `i` and `j` exists in `ComplexShape` `c`, then `i` is the 'previous' element of `j` in the `ComplexShape`.
More concisely: For any `ComplexShape` `c` and elements `i` and `j` of its index type `ι`, if there is a relation from `i` to `j` in `ComplexShape` `c`, then `prev c i = j`.
|
ComplexShape.next_eq'
theorem ComplexShape.next_eq' : ∀ {ι : Type u_1} (c : ComplexShape ι) {i j : ι}, c.Rel i j → c.next i = j
The theorem `ComplexShape.next_eq'` states that for any type `ι`, given a `ComplexShape` `c` of type `ι` and any two elements `i` and `j` of type `ι`, if the relation `Rel` defined on the `ComplexShape` `c` holds between `i` and `j`, then the `next` function on the `ComplexShape` `c` applied to `i` will return `j`. In simpler terms, if `j` is a "successor" of `i` according to the relationship defined by the `ComplexShape`, then the `next` function will return `j` when applied to `i`.
More concisely: For any `ComplexShape` `c` and elements `i` and `j` of type `ι` in it, if `Rel` holds between `i` and `j` on `c`, then `next c i = j`.
|
ComplexShape.next_eq
theorem ComplexShape.next_eq :
∀ {ι : Type u_1} (self : ComplexShape ι) {i j j' : ι}, self.Rel i j → self.Rel i j' → j = j'
The theorem `ComplexShape.next_eq` states that, for any type `ι`, given a `ComplexShape` of `ι`, and any three elements `i`, `j`, and `j'` of type `ι`, if both `j` and `j'` are related to `i` in the `ComplexShape`, then `j` must be equal to `j'`. In other words, from any given point `i` in the `ComplexShape`, there can be at most one distinct point `j` to which `i` is related.
More concisely: In a ComplexShape, for any type ι and any distinct points i, j, j' of type ι related to i, j = j'.
|