---

Step * of Lemma path-comp-prod

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) }

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))@i
6. g : Point(Path(A × B))@i
7. f@r1 ≡ g@r0
⊢ ∃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  \mtimes{}  B))


By

---

Latex:
(Auto  THEN  All  (Unfold  `path-comp-property`)  THEN  Intros)

---

Home Index