Step
*
1
1
of Lemma
ss-free-homotopic_inversion
1. X : SeparationSpace@i'
2. a : Point(X)@i
3. b : Point(X)@i
4. p : Point(Path(X))@i
5. p@r0 ≡ a
6. p@r1 ≡ b
7. t : {x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} @i
8. t' : {x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} @i
9. t ≡ t'
⊢ p@r1 - t ≡ p@r1 - t'
BY
{ (BLemma `path-at_functionality` THEN Auto) }
1
1. X : SeparationSpace@i'
2. a : Point(X)@i
3. b : Point(X)@i
4. p : Point(Path(X))@i
5. p@r0 ≡ a
6. p@r1 ≡ b
7. t : {x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} @i
8. t' : {x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} @i
9. t ≡ t'
⊢ (r1 - t) = (r1 - t')
Latex:
Latex:
1. X : SeparationSpace@i'
2. a : Point(X)@i
3. b : Point(X)@i
4. p : Point(Path(X))@i
5. p@r0 \mequiv{} a
6. p@r1 \mequiv{} b
7. t : \{x:\mBbbR{}| (r0 \mleq{} x) \mwedge{} (x \mleq{} r1)\} @i
8. t' : \{x:\mBbbR{}| (r0 \mleq{} x) \mwedge{} (x \mleq{} r1)\} @i
9. t \mequiv{} t'
\mvdash{} p@r1 - t \mequiv{} p@r1 - t'
By
Latex:
(BLemma `path-at\_functionality` THEN Auto)
Home
Index