Nuprl Definition : face-term-implies
Gamma ⊢ (phi ⇒ psi) ==
∀I:fset(ℕ). ∀rho:Gamma(I). ((phi(rho) = 1 ∈ Point(face_lattice(I))) ⇒ (psi(rho) = 1 ∈ Point(face_lattice(I))))
Definitions occuring in Statement :
cubical-term-at: u(a),
face_lattice: face_lattice(I),
I_cube: A(I),
lattice-1: 1,
lattice-point: Point(l),
fset: fset(T),
nat: ℕ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
equal: s = t ∈ T
Definitions occuring in definition :
fset: fset(T),
nat: ℕ,
all: ∀x:A. B[x],
I_cube: A(I),
implies: P ⇒ Q,
equal: s = t ∈ T,
lattice-point: Point(l),
cubical-term-at: u(a),
lattice-1: 1,
face_lattice: face_lattice(I)
FDL editor aliases :
face-term-implies
Latex:
Gamma \mvdash{} (phi {}\mRightarrow{} psi) == \mforall{}I:fset(\mBbbN{}). \mforall{}rho:Gamma(I). ((phi(rho) = 1) {}\mRightarrow{} (psi(rho) = 1))
Date html generated:
2016_05_19-AM-08_28_06
Last ObjectModification:
2016_03_04-PM-11_37_28
Theory : cubical!type!theory
Home
Index