Step
*
3
1
of Lemma
path-comp-union
1. A : SeparationSpace
2. B : SeparationSpace
3. v : Point(A + B)
4. v1 : Point(A + B)
5. v ≡ v1
⊢ (↑isr(v1))
⇒ (↑isl(v))
⇒ False
BY
{ (RepUR ``ss-point union-ss mk-ss`` -3
THEN RepUR ``ss-point union-ss mk-ss`` -2
THEN D -3
THEN D -2
THEN Reduce 0
THEN RepUR ``ss-eq ss-sep union-ss mk-ss union-sep`` -1
THEN Auto) }
Latex:
Latex:
1. A : SeparationSpace
2. B : SeparationSpace
3. v : Point(A + B)
4. v1 : Point(A + B)
5. v \mequiv{} v1
\mvdash{} (\muparrow{}isr(v1)) {}\mRightarrow{} (\muparrow{}isl(v)) {}\mRightarrow{} False
By
Latex:
(RepUR ``ss-point union-ss mk-ss`` -3
THEN RepUR ``ss-point union-ss mk-ss`` -2
THEN D -3
THEN D -2
THEN Reduce 0
THEN RepUR ``ss-eq ss-sep union-ss mk-ss union-sep`` -1
THEN Auto)
Home
Index