Nuprl Lemma : rng_prod_injection
∀[r:CRng]. ∀[n:ℕ]. ∀[F:ℕn ⟶ |r|]. ∀[f:ℕn →⟶ ℕn]. ((Π(r) 0 ≤ i < n. F[i]) = (Π(r) 0 ≤ i < n. F[f i]) ∈ |r|)
Proof
Error : references
Latex:
\mforall{}[r:CRng]. \mforall{}[n:\mBbbN{}]. \mforall{}[F:\mBbbN{}n {}\mrightarrow{} |r|]. \mforall{}[f:\mBbbN{}n \mrightarrow{}{}\mrightarrow{} \mBbbN{}n].
((\mPi{}(r) 0 \mleq{} i < n. F[i]) = (\mPi{}(r) 0 \mleq{} i < n. F[f i]))
Date html generated:
2020_05_20-AM-09_03_40
Last ObjectModification:
2020_01_10-PM-02_07_20
Theory : matrices
Home
Index