Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Iris
Iris
Commits
4cb0d91d
Commit
4cb0d91d
authored
Dec 10, 2017
by
Ralf Jung
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
fix a LeTeX warning
parent
3f321758
Pipeline
#5809
passed with stages
in 6 minutes and 25 seconds
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
3 additions
and
1 deletion
+3
-1
docs/constructions.tex
docs/constructions.tex
+3
-1
No files found.
docs/constructions.tex
View file @
4cb0d91d
...
...
@@ -34,7 +34,9 @@ $\UPred(-)$ is a locally non-expansive functor from $\CMRAs$ to $\COFEs$.
It is worth noting that the above quotient admits canonical
representatives. More precisely, one can show that every
equivalence class contains exactly one element
$
P
_
0
$
such that:
\[
\All
n,
\melt
.
(
\mval
(
\melt
)
\nincl
{
n
}
P
_
0
(
\melt
))
\Ra
n
\in
P
_
0
(
\melt
)
\tagH
{
UPred
-
canonical
}
\]
\begin{align*}
\All
n,
\melt
. (
\mval
(
\melt
)
\nincl
{
n
}
P
_
0(
\melt
))
\Ra
n
\in
P
_
0(
\melt
)
\tagH
{
UPred-canonical
}
\end{align*}
Intuitively, this says that
$
P
_
0
$
trivially holds whenever the resource is invalid.
Starting from any element
$
P
$
, one can find this canonical
representative by choosing
$
P
_
0
(
\melt
)
:
=
\setComp
{
n
}{
n
\in
\mval
(
\melt
)
\Ra
n
\in
P
(
\melt
)
}$
.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment