pouya/coalgebraic-simulation
2
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

mino

Browse Source
This commit is contained in:
Pouya
2026-08-04 03:23:25 +01:00
parent ac4a5ec5a1
commit 4f6689a096
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
draft/draft.tex
+1 -1
View File
@@ -483,7 +483,7 @@ We want to say that a natural order structure entails an order over a functor de
\begin{proof} \begin{proof}
$(I)$ Assuming $t\mathrel{(Ff\comp\sappr)} x$, there exists $s$ such that $t\sappr s$ and $Ff(s)=x$. Since $\appr$ is liftable, and thus natural, by~\autoref{def:nat-ord}, from $s\appr t$ we get $x\appr Ff(t)$ that is $t\mathrel{(\sappr\comp Ff)} x$. $(I)$ Assuming $t\mathrel{(Ff\comp\sappr)} x$, there exists $s$ such that $t\sappr s$ and $Ff(s)=x$. Since $\appr$ is liftable, and thus natural, by~\autoref{def:nat-ord}, from $s\appr t$ we get $x\appr Ff(t)$ that is $t\mathrel{(\sappr\comp Ff)} x$.
Assuming $t\mathrel{(\sappr\comp Ff)} x$, there exists $y$ such that $Ff(t)=y$ and $y\sappr x$. By~\autoref{def:liftable-ord} since $Ff(t)\sappr x$ there exists $s$ that $t\sappr s$ and $Ff(s)=x$ that is $t\mathrel{(Ff\comp\appr)}s$. Assuming $t\mathrel{(\sappr\comp Ff)} x$, there exists $y$ such that $Ff(t)=y$ and $y\sappr x$. By~\autoref{def:liftable-ord} since $Ff(t)\sappr x$ there exists $s$ that $t\sappr s$ and $Ff(s)=x$ that is $t\mathrel{(Ff\comp\sappr)}s$.
$(II)$ Basically, by definition of $\op$ and relation composition we have $(II)$ Basically, by definition of $\op$ and relation composition we have
\begin{gather*} \begin{gather*}