Nuprl Definition : real-cube-complex
RealCubeComplex(k) ==
T:Type
× finite(T)
× f:T ⟶ real-cube(k)
× (∀t1,t2:T. ((¬(t1 = t2 ∈ T)) ⇒ (adjacent-cubes(k;f t1;f t2) ∨ f t1 # f t2)))
Definitions occuring in Statement :
adjacent-cubes: adjacent-cubes(k;c1;c2),
real-cube-sep: c1 # c2,
real-cube: real-cube(k),
finite: finite(T),
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
or: P ∨ Q,
apply: f a,
function: x:A ⟶ B[x],
product: x:A × B[x],
universe: Type,
equal: s = t ∈ T
Definitions occuring in definition :
universe: Type,
finite: finite(T),
product: x:A × B[x],
function: x:A ⟶ B[x],
real-cube: real-cube(k),
all: ∀x:A. B[x],
implies: P ⇒ Q,
not: ¬A,
equal: s = t ∈ T,
or: P ∨ Q,
adjacent-cubes: adjacent-cubes(k;c1;c2),
real-cube-sep: c1 # c2,
apply: f a
FDL editor aliases :
real-cube-complex
Latex:
RealCubeComplex(k) ==
T:Type
\mtimes{} finite(T)
\mtimes{} f:T {}\mrightarrow{} real-cube(k)
\mtimes{} (\mforall{}t1,t2:T. ((\mneg{}(t1 = t2)) {}\mRightarrow{} (adjacent-cubes(k;f t1;f t2) \mvee{} f t1 \# f t2)))
Date html generated:
2019_10_30-AM-11_31_40
Last ObjectModification:
2019_09_30-AM-11_18_03
Theory : real!vectors
Home
Index