---

Step * of Lemma product-discrete

∀A:Type. ∀B:A ⟶ Type.  (discrete-type(A) ⇒ (∀a:A. discrete-type(B[a])) ⇒ discrete-type(a:A × B[a]))
BY
{ (Auto
   THEN (D 0 THEN Auto)
   THEN (Assert ∀x,y:ℝ.  ((fst((f x))) = (fst((f y))) ∈ A) BY
               (Auto
                THEN (D 3 With ⌜λx.(fst((f x)))⌝  THENA Auto)
                THEN Reduce -1
                THEN D -1
                THEN Auto
                THEN EqCD
                THEN Auto))) }

1
1. A : Type
2. B : A ⟶ Type
3. discrete-type(A)
4. ∀a:A. discrete-type(B[a])
5. f : ℝ ⟶ (a:A × B[a])
6. ∀x,y:ℝ.  ((x = y) ⇒ ((f x) = (f y) ∈ (a:A × B[a])))
7. x : ℝ
8. y : ℝ
9. ∀x,y:ℝ.  ((fst((f x))) = (fst((f y))) ∈ A)
⊢ (f x) = (f y) ∈ (a:A × B[a])

---

Latex:

---

Latex:
\mforall{}A:Type.  \mforall{}B:A  {}\mrightarrow{}  Type.
    (discrete-type(A)  {}\mRightarrow{}  (\mforall{}a:A.  discrete-type(B[a]))  {}\mRightarrow{}  discrete-type(a:A  \mtimes{}  B[a]))


By

---

Latex:
(Auto
  THEN  (D  0  THEN  Auto)
  THEN  (Assert  \mforall{}x,y:\mBbbR{}.    ((fst((f  x)))  =  (fst((f  y))))  BY
                          (Auto
                            THEN  (D  3  With  \mkleeneopen{}\mlambda{}x.(fst((f  x)))\mkleeneclose{}    THENA  Auto)
                            THEN  Reduce  -1
                            THEN  D  -1
                            THEN  Auto
                            THEN  EqCD
                            THEN  Auto)))

---

Home Index