English
Fin n carries a BiheytingAlgebra structure (hence a Heyting algebra and a Coheyting algebra).
Русский
Fin n имеет структуру BiheytingAlgebra (то есть Heyting и Coheyting алгебры).
LaTeX
$$$\mathrm{BiheytingAlgebra}(\mathrm{Fin}(n))$$$
Lean4
instance instBiheytingAlgebra [NeZero n] : BiheytingAlgebra (Fin n) :=
LinearOrder.toBiheytingAlgebra
(Fin n)
/- There is a slight asymmetry here, in the sense that `0` is of type `Fin n` when we have
`[NeZero n]` whereas `last n` is of type `Fin (n + 1)`. To address this properly would
require a change to std4, defining `NeZero n` and thus re-defining `last n`
(and possibly make its argument implicit) as `rev 0`, of type `Fin n`. As we can see from these
lemmas, this would be equivalent to the existing definition. -/
