---

Step * of Lemma function-discrete

∀A:Type. ∀B:A ⟶ Type.  ((∀a:A. discrete-type(B[a])) ⇒ discrete-type(a:A ⟶ B[a]))
BY
{ (Auto THEN (D 0 THEN Auto) THEN (FunExt THENA Auto) THEN RenameVar `a' (-1)) }

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (D  0  THEN  Auto)  THEN  (FunExt  THENA  Auto)  THEN  RenameVar  `a'  (-1))

---

Home Index