---

Step * of Lemma path-comp-union

No Annotations
∀[A,B:SeparationSpace].  (path-comp-property(A) ⇒ path-comp-property(B) ⇒ path-comp-property(A + B))
BY
{ (Auto
   THEN All (Unfold `path-comp-property`)
   THEN Intros
   THEN (InstLemma `path-in-union` [⌜A⌝;⌜B⌝;⌜f⌝]⋅ THENA Auto)
   THEN (InstLemma `path-in-union` [⌜A⌝;⌜B⌝;⌜g⌝]⋅ THENA Auto)
   THEN SplitOrHyps) }

1
1. [A] : SeparationSpace
2. [B] : SeparationSpace
3. ∀f,g:Point(Path(A)).  (f@r1 ≡ g@r0 ⇒ (∃h:Point(Path(A)). path-comp-rel(A;f;g;h)))
4. ∀f,g:Point(Path(B)).  (f@r1 ≡ g@r0 ⇒ (∃h:Point(Path(B)). path-comp-rel(B;f;g;h)))
5. f : Point(Path(A + B))
6. g : Point(Path(A + B))
7. f@r1 ≡ g@r0
8. (∀x:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} . (↑isl(f@x))) ∧ (λx.outl(f x) ∈ Point(Path(A)))
9. (∀x:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} . (↑isl(g@x))) ∧ (λx.outl(g x) ∈ Point(Path(A)))
⊢ ∃h:Point(Path(A + B)). path-comp-rel(A + B;f;g;h)

2
1. [A] : SeparationSpace
2. [B] : SeparationSpace
3. ∀f,g:Point(Path(A)).  (f@r1 ≡ g@r0 ⇒ (∃h:Point(Path(A)). path-comp-rel(A;f;g;h)))
4. ∀f,g:Point(Path(B)).  (f@r1 ≡ g@r0 ⇒ (∃h:Point(Path(B)). path-comp-rel(B;f;g;h)))
5. f : Point(Path(A + B))
6. g : Point(Path(A + B))
7. f@r1 ≡ g@r0
8. (∀x:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} . (↑isr(f@x))) ∧ (λx.outr(f x) ∈ Point(Path(B)))
9. (∀x:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} . (↑isl(g@x))) ∧ (λx.outl(g x) ∈ Point(Path(A)))
⊢ ∃h:Point(Path(A + B)). path-comp-rel(A + B;f;g;h)

3
1. [A] : SeparationSpace
2. [B] : SeparationSpace
3. ∀f,g:Point(Path(A)).  (f@r1 ≡ g@r0 ⇒ (∃h:Point(Path(A)). path-comp-rel(A;f;g;h)))
4. ∀f,g:Point(Path(B)).  (f@r1 ≡ g@r0 ⇒ (∃h:Point(Path(B)). path-comp-rel(B;f;g;h)))
5. f : Point(Path(A + B))
6. g : Point(Path(A + B))
7. f@r1 ≡ g@r0
8. (∀x:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} . (↑isl(f@x))) ∧ (λx.outl(f x) ∈ Point(Path(A)))
9. (∀x:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} . (↑isr(g@x))) ∧ (λx.outr(g x) ∈ Point(Path(B)))
⊢ ∃h:Point(Path(A + B)). path-comp-rel(A + B;f;g;h)

4
1. [A] : SeparationSpace
2. [B] : SeparationSpace
3. ∀f,g:Point(Path(A)).  (f@r1 ≡ g@r0 ⇒ (∃h:Point(Path(A)). path-comp-rel(A;f;g;h)))
4. ∀f,g:Point(Path(B)).  (f@r1 ≡ g@r0 ⇒ (∃h:Point(Path(B)). path-comp-rel(B;f;g;h)))
5. f : Point(Path(A + B))
6. g : Point(Path(A + B))
7. f@r1 ≡ g@r0
8. (∀x:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} . (↑isr(f@x))) ∧ (λx.outr(f x) ∈ Point(Path(B)))
9. (∀x:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} . (↑isr(g@x))) ∧ (λx.outr(g x) ∈ Point(Path(B)))
⊢ ∃h:Point(Path(A + B)). path-comp-rel(A + B;f;g;h)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A,B:SeparationSpace].
    (path-comp-property(A)  {}\mRightarrow{}  path-comp-property(B)  {}\mRightarrow{}  path-comp-property(A  +  B))


By

---

Latex:
(Auto
  THEN  All  (Unfold  `path-comp-property`)
  THEN  Intros
  THEN  (InstLemma  `path-in-union`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `path-in-union`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  SplitOrHyps)

---

Home Index