---

Step * of Lemma path-comp-for-reals

No Annotations
path-comp-property(ℝ)
BY
{ (((D 0 THEN Auto) THEN (All (RWO "path-ss-point") THENA Auto))
   THEN (InstLemma `real-path-comp-exists` [⌜f⌝;⌜g⌝]⋅ THENA Auto)
   THEN RepUR ``path-comp-rel path-at`` 0
   THEN All (RepUR ``ss-point ss-eq ss-sep real-ss mk-ss unit-ss set-ss``)
   THEN Try ((All Reduce
              THEN Unfold `r-ap` 0
              THEN BLemma `not-rneq`
              THEN Auto
              THEN DSetVars
              THEN Auto
              THEN BackThruSomeHyp
              THEN EAuto 1))
   THEN ExRepD
   THEN D 0 With ⌜h⌝ ) }

1
.....wf..... 
1. f : {f:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ ℝ| ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  ((¬t ≠ t') ⇒ (¬f t ≠ f t'))} 
2. g : {f:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ ℝ| ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  ((¬t ≠ t') ⇒ (¬f t ≠ f t'))} 
3. ¬f@r1 ≠ g@r0
4. h : [r0, r1] ⟶ℝ
5. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (h(t) = f(r(2) * t))
6. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (h(t) = g((r(2) * t) - r1))
7. ∀x,y:{x:ℝ| x ∈ [r0, r1]} .  ((x = y) ⇒ (h(x) = h(y)))
⊢ h ∈ {f:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ ℝ| ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  ((¬t ≠ t') ⇒ (¬f t ≠ f t'))} 

2
1. f : {f:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ ℝ| ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  ((¬t ≠ t') ⇒ (¬f t ≠ f t'))} 
2. g : {f:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ ℝ| ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  ((¬t ≠ t') ⇒ (¬f t ≠ f t'))} 
3. ¬f@r1 ≠ g@r0
4. h : [r0, r1] ⟶ℝ
5. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (h(t) = f(r(2) * t))
6. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (h(t) = g((r(2) * t) - r1))
7. ∀x,y:{x:ℝ| x ∈ [r0, r1]} .  ((x = y) ⇒ (h(x) = h(y)))
⊢ (∀t:{x:ℝ| (r0 ≤ x) ∧ (x ≤ (r1/r(2)))} . (¬h t ≠ f (r(2) * t)))
∧ (∀t:{x:ℝ| ((r1/r(2)) ≤ x) ∧ (x ≤ r1)} . (¬h t ≠ g ((r(2) * t) - r1)))

3
.....wf..... 
1. f : {f:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ ℝ| ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  ((¬t ≠ t') ⇒ (¬f t ≠ f t'))} 
2. g : {f:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ ℝ| ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  ((¬t ≠ t') ⇒ (¬f t ≠ f t'))} 
3. ¬f@r1 ≠ g@r0
4. h : [r0, r1] ⟶ℝ
5. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (h(t) = f(r(2) * t))
6. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (h(t) = g((r(2) * t) - r1))
7. ∀x,y:{x:ℝ| x ∈ [r0, r1]} .  ((x = y) ⇒ (h(x) = h(y)))
8. h1 : {f:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ ℝ| ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  ((¬t ≠ t') ⇒ (¬f t ≠ f t'))} 
⊢ istype((∀t:{x:ℝ| (r0 ≤ x) ∧ (x ≤ (r1/r(2)))} . (¬h1 t ≠ f (r(2) * t)))
∧ (∀t:{x:ℝ| ((r1/r(2)) ≤ x) ∧ (x ≤ r1)} . (¬h1 t ≠ g ((r(2) * t) - r1))))

---

Latex:

---

Latex:
No  Annotations
path-comp-property(\mBbbR{})


By

---

Latex:
(((D  0  THEN  Auto)  THEN  (All  (RWO  "path-ss-point")  THENA  Auto))
  THEN  (InstLemma  `real-path-comp-exists`  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepUR  ``path-comp-rel  path-at``  0
  THEN  All  (RepUR  ``ss-point  ss-eq  ss-sep  real-ss  mk-ss  unit-ss  set-ss``)
  THEN  Try  ((All  Reduce
                        THEN  Unfold  `r-ap`  0
                        THEN  BLemma  `not-rneq`
                        THEN  Auto
                        THEN  DSetVars
                        THEN  Auto
                        THEN  BackThruSomeHyp
                        THEN  EAuto  1))
  THEN  ExRepD
  THEN  D  0  With  \mkleeneopen{}h\mkleeneclose{}  )

---

Home Index