Nuprl Definition : immediate-rc-face
immediate-rc-face(k;f;c) == f ≤ c ∧ (dim(f) = (dim(c) - 1) ∈ ℤ)
Definitions occuring in Statement :
rat-cube-dimension: dim(c),
rat-cube-face: c ≤ d,
and: P ∧ Q,
subtract: n - m,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
natural_number: $n,
rat-cube-dimension: dim(c),
subtract: n - m,
int: ℤ,
equal: s = t ∈ T,
rat-cube-face: c ≤ d,
and: P ∧ Q
FDL editor aliases :
immediate-rc-face
Latex:
immediate-rc-face(k;f;c) == f \mleq{} c \mwedge{} (dim(f) = (dim(c) - 1))
Date html generated:
2019_10_29-AM-07_53_41
Last ObjectModification:
2019_10_17-PM-02_55_51
Theory : rationals
Home
Index