---

Step * of Lemma compact-product

∀[T:Type]. ∀[S:T ⟶ Type].  (compact-type(T) ⇒ (∀t:T. compact-type(S[t])) ⇒ compact-type(t:T × S[t]))
BY
{ (Auto THEN All (Unfold `compact-type`)⋅ THEN D 0 THEN Auto) }

1
1. [T] : Type
2. [S] : T ⟶ Type
3. ∀p:T ⟶ 𝔹. ((∃x:T. p x = ff) ∨ (∀x:T. p x = tt))
4. ∀t:T. ∀p:S[t] ⟶ 𝔹.  ((∃x:S[t]. p x = ff) ∨ (∀x:S[t]. p x = tt))
5. p : (t:T × S[t]) ⟶ 𝔹
⊢ (∃x:t:T × S[t]. p x = ff) ∨ (∀x:t:T × S[t]. p x = tt)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[S:T  {}\mrightarrow{}  Type].
    (compact-type(T)  {}\mRightarrow{}  (\mforall{}t:T.  compact-type(S[t]))  {}\mRightarrow{}  compact-type(t:T  \mtimes{}  S[t]))


By

---

Latex:
(Auto  THEN  All  (Unfold  `compact-type`)\mcdot{}  THEN  D  0  THEN  Auto)

---

Home Index