Series of a relation #
If r
is a relation on α
then a relation series of length n
is a series
a_0, a_1, ..., a_n
such that r a_i a_{i+1}
for all i < n
- length : ℕ
The number of inequalities in the series
The underlying function of a relation series
- step : ∀ (i : Fin s.length), r (RelSeries.toFun s (Fin.castSucc i)) (RelSeries.toFun s (Fin.succ i))
Adjacent elements are related
Let r
be a relation on α
, a relation series of r
of length n
is a series
a_0, a_1, ..., a_n
such that r a_i a_{i+1}
for all i < n
Instances For
For any type α
, each term of α
gives a relation series with the right most index to be 0.
Instances For
Every nonempty list satisfying the chain condition gives a relation series
Instances For
Relation series of r
and nonempty list of α
satisfying r
-chain condition bijectively
corresponds to each other.
Instances For
A relation
r
is said to be finite dimensional iff there is a relation series ofr
with the maximum length.
A relation r
is said to be finite dimensional iff there is a relation series of r
with the
maximum length.
Instances
A relation
r
is said to be infinite dimensional iff there exists relation series of arbitrary length.
A relation r
is said to be infinite dimensional iff there exists relation series of arbitrary
length.
Instances
The longest relational series when a relation is finite dimensional
Instances For
A relation series with length n
if the relation is infinite dimensional
Instances For
If a relation on α
is infinite dimensional, then α
is nonempty.
The longest <
-series when a type is finite dimensional
Instances For
A <
-series with length n
if the relation is infinite dimensional
Instances For
if α
is infinite dimensional, then α
is nonempty.