Nuprl Lemma : select-firstn

∀[L:Top List]. ∀[n:ℕ]. ∀[x:ℕn].  (firstn(n;L)[x] ~ L[x])


Proof

Error : references
Latex:
\mforall{}[L:Top  List].  \mforall{}[n:\mBbbN{}].  \mforall{}[x:\mBbbN{}n].    (firstn(n;L)[x]  \msim{}  L[x])


Date html generated: 2020_05_19-PM-09_37_36
Last ObjectModification: 2020_03_05-AM-10_50_17

Theory : list_0


Home Index