Nuprl Lemma : generic-non-empty
∀[T:Type]. ∀[S:(ℕ ⟶ T) ⟶ ℙ'].  (T 
⇒ Generic{f:ℕ⟶T|S[f]} 
⇒ (∃f:ℕ ⟶ T. S[f]))
Proof
Error : references
Latex:
\mforall{}[T:Type].  \mforall{}[S:(\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbP{}'].    (T  {}\mRightarrow{}  Generic\{f:\mBbbN{}{}\mrightarrow{}T|S[f]\}  {}\mRightarrow{}  (\mexists{}f:\mBbbN{}  {}\mrightarrow{}  T.  S[f]))
Date html generated:
2020_05_20-AM-08_41_03
Last ObjectModification:
2020_02_07-AM-09_16_08
Theory : general
Home
Index