---

Definition: ss-homeo
ss-homeo(X;Y) ==  ∃f:Point(X ⟶ Y). ∃g:Point(Y ⟶ X). ((∀x:Point(X). g(f(x)) ≡ x) ∧ (∀y:Point(Y). f(g(y)) ≡ y))

Lemma: ss-homeo_wf
∀[X,Y:SeparationSpace].  (ss-homeo(X;Y) ∈ ℙ)

Lemma: ss-homeo_weakening
∀[X,Y:SeparationSpace].  ss-homeo(X;Y) supposing X = Y ∈ SeparationSpace

Lemma: ss-homeo_inversion
∀[X,Y:SeparationSpace].  (ss-homeo(X;Y) ⇒ ss-homeo(Y;X))

Lemma: ss-homeo_transitivity
∀[X,Y,Z:SeparationSpace].  (ss-homeo(X;Y) ⇒ ss-homeo(Y;Z) ⇒ ss-homeo(X;Z))

Lemma: ss-fun-fun
∀[X,Y,Z:SeparationSpace].  ss-homeo(X ⟶ Y ⟶ Z;X × Y ⟶ Z)

Lemma: ss-prod-prod
∀[X,Y,Z:SeparationSpace].  ss-homeo(X × Y × Z;X × Y × Z)

Lemma: unit-ss-eq
∀[t,t':{t:ℝ| t ∈ [r0, r1]} ].  uiff(t = t';t ≡ t')

Definition: path-ss
Path(X) ==  𝕀 ⟶ X

Lemma: path-ss_wf
∀[X:SeparationSpace]. (Path(X) ∈ SeparationSpace)

Lemma: path-ss-point
∀[X:Top]
  (Point(Path(X)) ~ {f:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ Point(X)| ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  (t ≡ t' ⇒ f t ≡ f t\000C')} )

Definition: path-at
p@t ==  p t

Lemma: path-at_wf
∀[X:SeparationSpace]. ∀[p:Point(Path(X))]. ∀[t:{t:ℝ| t ∈ [r0, r1]} ].  (p@t ∈ Point(X))

Lemma: path-at_functionality
∀[X:SeparationSpace]. ∀[p:Point(Path(X))]. ∀[t,t':{t:ℝ| t ∈ [r0, r1]} ].  p@t ≡ p@t' supposing t = t'

Lemma: path-at_functionality2
∀[X:SeparationSpace]. ∀[p:Point(Path(X))]. ∀[t,t':{t:ℝ| t ∈ [r0, r1]} ].  p@t ≡ p@t' supposing t ≡ t'

Definition: ss-free-homotopic
ss-free-homotopic(X;a;b) ==  ∃p:Point(Path(X)). (p@r0 ≡ a ∧ p@r1 ≡ b)

Lemma: ss-free-homotopic_wf
∀[X:SeparationSpace]. ∀[a,b:Point(X)].  (ss-free-homotopic(X;a;b) ∈ ℙ)

Lemma: ss-free-homotopic_weakening
∀X:SeparationSpace. ∀a,b:Point(X).  ss-free-homotopic(X;a;b) supposing a ≡ b

Lemma: ss-free-homotopic_inversion
∀X:SeparationSpace. ∀a,b:Point(X).  (ss-free-homotopic(X;a;b) ⇒ ss-free-homotopic(X;b;a))

Definition: ss-homotopic
ss-homotopic(X;x0;x1;a;b) ==
  ∃p:Point(Path(Path(X))). (p@r0 ≡ a ∧ p@r1 ≡ b ∧ (∀t:{t:ℝ| t ∈ [r0, r1]} . (p@t@r0 ≡ x0 ∧ p@t@r1 ≡ x1)))

Lemma: ss-homotopic_wf
∀[X:SeparationSpace]. ∀[x0,x1:Point(X)]. ∀[a,b:Point(Path(X))].  (ss-homotopic(X;x0;x1;a;b) ∈ ℙ)

Lemma: ss-homotopic_weakening
∀X:SeparationSpace
  ∀[x0,x1:Point(X)].  ∀a,b:Point(Path(X)).  (ss-homotopic(X;x0;x1;a;b)) supposing (a ≡ b and b@r0 ≡ x0 and b@r1 ≡ x1)

Lemma: ss-homotopic_inversion
∀X:SeparationSpace. ∀[x0,x1:Point(X)].  ∀a,b:Point(Path(X)).  (ss-homotopic(X;x0;x1;a;b) ⇒ ss-homotopic(X;x0;x1;b;a))

Definition: path-comp-rel
path-comp-rel(X;f;g;h) ==
  (∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . h@t ≡ f@r(2) * t) ∧ (∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . h@t ≡ g@(r(2) * t) - r1)

Lemma: path-comp-rel_wf
∀[X:SeparationSpace]. ∀[f,g,h:Point(Path(X))].  (path-comp-rel(X;f;g;h) ∈ ℙ)

Definition: path-comp-property
path-comp-property(X) ==  ∀f,g:Point(Path(X)).  (f@r1 ≡ g@r0 ⇒ (∃h:Point(Path(X)). path-comp-rel(X;f;g;h)))

Lemma: path-comp-property_wf
∀[X:SeparationSpace]. (path-comp-property(X) ∈ ℙ)

Lemma: path-comp-property_functionality
∀[X,Y:SeparationSpace].  (ss-homeo(X;Y) ⇒ (path-comp-property(X) ⇐⇒ path-comp-property(Y)))

Lemma: path-comp-for-reals
path-comp-property(ℝ)

Lemma: path-comp-prod
∀[A,B:SeparationSpace].  (path-comp-property(A) ⇒ path-comp-property(B) ⇒ path-comp-property(A × B))

Lemma: path-in-union
∀[A,B:SeparationSpace].
  ∀f:Point(Path(A + B))
    (((∀x:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} . (↑isl(f@x))) ∧ (λx.outl(f x) ∈ Point(Path(A))))
    ∨ ((∀x:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} . (↑isr(f@x))) ∧ (λx.outr(f x) ∈ Point(Path(B)))))

Lemma: path-comp-union
∀[A,B:SeparationSpace].  (path-comp-property(A) ⇒ path-comp-property(B) ⇒ path-comp-property(A + B))

Lemma: path-comp-fun
∀[T:Type]. ∀[B:SeparationSpace].  (path-comp-property(B) ⇒ path-comp-property(T ⟶ B))

Lemma: path-comp-set
∀[A:SeparationSpace]. ∀[P:Point(A) ⟶ ℙ].
  ((∀a:Point(A). Stable{P[a]})
  ⇒ (∀a,b:Point(A).  (a ≡ b ⇒ P[b] ⇒ P[a]))
  ⇒ path-comp-property(A)
  ⇒ path-comp-property({a:A | P[a]}))

Definition: ss-basic
ss-basic(X) ==  (Point(X ⟶ ℝ) × ℝ) List

Lemma: ss-basic_wf
∀[X:SeparationSpace]. (ss-basic(X) ∈ Type)

Definition: ss-mem-basic
x ∈ B ==  (∀p∈B.let f,r = p in f(x) < r)

Lemma: ss-mem-basic_wf
∀[X:SeparationSpace]. ∀[B:ss-basic(X)]. ∀[x:Point(X)].  (x ∈ B ∈ ℙ)

Lemma: sq_stable__ss-mem-basic
∀[X:SeparationSpace]. ∀B:ss-basic(X). ∀x:Point(X).  SqStable(x ∈ B)

Definition: ss-open
Open(X) ==  ss-basic(X) ⟶ ℙ

Lemma: ss-open_wf
∀[X:SeparationSpace]. (Open(X) ∈ 𝕌')

Definition: ss-mem-open
x ∈ O ==  ∃B:ss-basic(X). ((O B) ∧ x ∈ B)

Lemma: ss-mem-open_wf
∀[X:SeparationSpace]. ∀[O:Open(X)]. ∀[x:Point(X)].  (x ∈ O ∈ ℙ)

Definition: ss-empty
ss-empty() ==  λB.False

Lemma: ss-empty_wf
∀[X:SeparationSpace]. (ss-empty() ∈ Open(X))

Lemma: ss-mem-empty
∀[X:SeparationSpace]. ∀[x:Point(X)].  uiff(x ∈ ss-empty();False)

Definition: ss-basic-whole
ss-basic-whole() ==  [<ss-const(r0), r1>]

Lemma: ss-basic-whole_wf
∀[X:SeparationSpace]. (ss-basic-whole() ∈ ss-basic(X))

Definition: ss-basic-and
ss-basic-and(u;v) ==  u @ v

Lemma: ss-basic-and_wf
∀[X:SeparationSpace]. ∀[u,v:ss-basic(X)].  (ss-basic-and(u;v) ∈ ss-basic(X))

Lemma: ss-mem-basic-and
∀[X:SeparationSpace]. ∀u,v:ss-basic(X). ∀x:Point(X).  uiff(x ∈ ss-basic-and(u;v);x ∈ u ∧ x ∈ v)

Lemma: ss-mem-basic-whole
∀X:SeparationSpace. ∀x:Point(X).  uiff(x ∈ ss-basic-whole();True)

Definition: ss-whole
ss-whole(X) ==  λB.(B = ss-basic-whole() ∈ ss-basic(X))

Lemma: ss-whole_wf
∀[X:SeparationSpace]. (ss-whole(X) ∈ Open(X))

Lemma: ss-mem-whole
∀X:SeparationSpace. ∀x:Point(X).  uiff(x ∈ ss-whole(X);True)

Definition: ss-open-and
A ⋂ B ==  λz.∃u,v:ss-basic(X). ((A u) ∧ (B v) ∧ (z = ss-basic-and(u;v) ∈ ss-basic(X)))

Lemma: ss-open-and_wf
∀[X:SeparationSpace]. ∀[A,B:Open(X)].  (A ⋂ B ∈ Open(X))

Lemma: ss-mem-open-and
∀[X:SeparationSpace]. ∀A,B:Open(X). ∀x:Point(X).  (x ∈ A ⋂ B ⇐⇒ x ∈ A ∧ x ∈ B)

Definition: ss-open-or
⋃x:T.F[x] ==  λB.∃x:T. (F[x] B)

Lemma: ss-open-or_wf
∀[X:SeparationSpace]. ∀[T:Type]. ∀[F:T ⟶ Open(X)].  (⋃x:T.F[x] ∈ Open(X))

Lemma: ss-mem-open-or
∀[X:SeparationSpace]. ∀T:Type. ∀F:T ⟶ Open(X). ∀x:Point(X).  (x ∈ ⋃t:T.F[t] ⇐⇒ ∃t:T. x ∈ F[t])

Lemma: path-end-mem-basic
∀X:SeparationSpace. ∀f:Point(Path(X)). ∀B:ss-basic(X).
  (f@r1 ∈ B ⇒ (∃z:{z:ℝ| z ∈ [r0, r1)} . ∀t:{t:ℝ| t ∈ [z, r1]} . f@t ∈ B))

Lemma: path-end-mem-open
∀X:SeparationSpace. ∀f:Point(Path(X)). ∀O:Open(X).
  (f@r1 ∈ O ⇒ (∃z:{z:ℝ| z ∈ [r0, r1)} . ∀t:{t:ℝ| t ∈ [z, r1]} . f@t ∈ O))



Home Index