Nuprl Lemma : nc-m-nc-0
∀[I:fset(ℕ)]. ∀[i:{i:ℕ| ¬i ∈ I} ]. ∀[j:{j:ℕ| ¬j ∈ I+i} ]. (m(i;j) ⋅ (j0) = (i0) ⋅ s ∈ I+i ⟶ I+i)
Proof
Error : references
Latex:
\mforall{}[I:fset(\mBbbN{})]. \mforall{}[i:\{i:\mBbbN{}| \mneg{}i \mmember{} I\} ]. \mforall{}[j:\{j:\mBbbN{}| \mneg{}j \mmember{} I+i\} ]. (m(i;j) \mcdot{} (j0) = (i0) \mcdot{} s)
Date html generated:
2020_05_21-AM-10_29_53
Last ObjectModification:
2019_12_10-AM-01_11_45
Theory : cubical!type!theory
Home
Index