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