ID | Name | Lemma | Duals |
FT1 | idempotence (as a consequence of distance idempotence) | $x+x=x$ | n/a |
FT2 | reflexivity (as a consequence of distance idempotence) | $x\leq x$ | n/a |
FT3 | transitivity (as a consequence of distance idempotence) | $x \leq y \wedge y \leq z \Rightarrow x \leq z$ | n/a |
FT4 | upper bound (as a consequence of distance idempotence) | $x \leq x+y$ $y \leq x+y$ |
n/a |
FT5 | supremum (sum split) (as a consequence of distance idempotence) | $x+y \leq z \Leftrightarrow x \leq z \wedge y \leq z$ | n/a |
FT6 | quasicommutativity (as a consequence of distance idempotence) | $\mbox{eqv}(x+y,y+x)$ | n/a |
FT7 | isotony (as a consequence of distance idempotence) | $x \leq y \Rightarrow x+z \leq y+z$ $x \leq y \Rightarrow z+x \leq z+y$ |
n/a |
FT8 | equivalence of superdistributivity and isotony (as a consequence of distance idempotence) | $\forall x \forall y.(f(x)+f(y) \leq f(x+y)) \Leftrightarrow \forall x \forall y.(x \leq y \Rightarrow f(x) \leq f(y))$ | n/a |
©2007. Peter Höfner |