---

Step * of Lemma compact-type-compact-type2

∀[T:Type]. (compact-type(T) ∧ T ⇐⇒ compact-type2(T))
BY
{ (Auto THEN All (RepUR ``compact-type compact-type2 p-selector``)⋅) }

1
1. [T] : Type
2. ∀p:T ⟶ 𝔹. ((∃x:T. p x = ff) ∨ (∀x:T. p x = tt))
3. T
⊢ ∀p:T ⟶ 𝔹. (∃x:{T| ((∃y:T. p y = ff) ⇒ p x = ff)})

2
1. [T] : Type
2. ∀p:T ⟶ 𝔹. (∃x:{T| ((∃y:T. p y = ff) ⇒ p x = ff)})
⊢ ∀p:T ⟶ 𝔹. ((∃x:T. p x = ff) ∨ (∀x:T. p x = tt))

3
1. [T] : Type
2. ∀p:T ⟶ 𝔹. (∃x:{T| ((∃y:T. p y = ff) ⇒ p x = ff)})
⊢ T

---

Latex:

---

Latex:
\mforall{}[T:Type].  (compact-type(T)  \mwedge{}  T  \mLeftarrow{}{}\mRightarrow{}  compact-type2(T))


By

---

Latex:
(Auto  THEN  All  (RepUR  ``compact-type  compact-type2  p-selector``)\mcdot{})

---

Home Index