foreign notation: replace "D \text{ s.t. } \isforeign{D}" with "D \in \foreign"

[topbloke-formulae.git] / pseudomerge.tex

diff --git a/pseudomerge.tex b/pseudomerge.tex
index 1e9422c447b6f143837553c40a9afefe2cfeeed4..0decb5f023c73c701f4d940c0ffc28d923791f54 100644 (file)
--- a/pseudomerge.tex
+++ b/pseudomerge.tex
@@ -25,7 +25,7 @@ but whose contents are exactly those of $L$.
 }\]
 
 \[ \eqn{ Foreign Unaffected }{
- \bigforall_{ D \text{ s.t. } \patchof{D} = \bot }
+ \bigforall_{ D \in \foreign }
   \left[ \bigexists_{A \in \set A} D \le A \right]
    \implies
   D \le L
@@ -34,7 +34,7 @@ but whose contents are exactly those of $L$.
 
 \subsection{Lemma: Foreign Identical}
 
-$\patchof{D} = \bot \implies \big[ D \le C \equiv D \le L \big]$.
+$\isforeign{D} \implies \big[ D \le C \equiv D \le L \big]$.
 
 \proof{
 If $D \le L$, trivially $D \le C$; so conversely