Nuprl Lemma : rat-cube-sub-complex_wf
∀[k,n:ℕ]. ∀[K:n-dim-complex]. ∀[P:{x:ℚCube(k)| (x ∈ K)} ⟶ 𝔹]. (rat-cube-sub-complex(P;K) ∈ n-dim-complex)
Proof
Error : references
Latex:
\mforall{}[k,n:\mBbbN{}]. \mforall{}[K:n-dim-complex]. \mforall{}[P:\{x:\mBbbQ{}Cube(k)| (x \mmember{} K)\} {}\mrightarrow{} \mBbbB{}].
(rat-cube-sub-complex(P;K) \mmember{} n-dim-complex)
Date html generated:
2020_05_20-AM-09_21_45
Last ObjectModification:
2019_10_17-PM-02_31_43
Theory : rationals
Home
Index