A rank whose values do not grow along the even lengths, so that ranking the even lengths descending reads them upwards. Derived, not registered per rank: a family's occurrences in the words of length N are \((N - n + 1)\) offsets times its density times \(|\Sigma|^N\), a product of non-negative sequences that do not grow, which does not grow either. The product law, stated here for the join's exact count; a general one belongs in :posetal, on an exact carrier or on an extent, since a word's × wraps and an antitone product past it is not antitone (#1134).
More...
Detailed Description
struct dedekind::category::antitone_on_even_lengths< Rank >
A rank whose values do not grow along the even lengths, so that ranking the even lengths descending reads them upwards. Derived, not registered per rank: a family's occurrences in the words of length N are \((N - n + 1)\) offsets times its density times \(|\Sigma|^N\), a product of non-negative sequences that do not grow, which does not grow either. The product law, stated here for the join's exact count; a general one belongs in :posetal, on an exact carrier or on an extent, since a word's × wraps and an antitone product past it is not antitone (#1134).
- Template Parameters
-
Rank the rank.
The documentation for this struct was generated from the following file:
- src/main/modules/dedekind/category/comprehension.cppm
