---

Step * of Lemma path-comp-fun

No Annotations
∀[T:Type]. ∀[B:SeparationSpace].  (path-comp-property(B) ⇒ path-comp-property(T ⟶ B))
BY
{ (Auto THEN All (Unfold `path-comp-property`) THEN Intros) }

1
1. [T] : Type
2. [B] : SeparationSpace
3. ∀f,g:Point(Path(B)).  (f@r1 ≡ g@r0 ⇒ (∃h:Point(Path(B)). path-comp-rel(B;f;g;h)))
4. f : Point(Path(T ⟶ B))
5. g : Point(Path(T ⟶ B))
6. f@r1 ≡ g@r0
⊢ ∃h:Point(Path(T ⟶ B)). path-comp-rel(T ⟶ B;f;g;h)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[B:SeparationSpace].    (path-comp-property(B)  {}\mRightarrow{}  path-comp-property(T  {}\mrightarrow{}  B))


By

---

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

---

Home Index