### Nuprl Lemma : face-cube_wf

`∀[X:CubicalSet]. ∀[I:Cname List]. ∀[f:I-face(X;I)].  (cube(f) ∈ X(I-[dimension(f)]))`

Proof

Definitions occuring in Statement :  face-cube: `cube(f)` face-dimension: `dimension(f)` I-face: `I-face(X;I)` I-cube: `X(I)` cubical-set: `CubicalSet` cname_deq: `CnameDeq` coordinate_name: `Cname` list-diff: `as-bs` cons: `[a / b]` nil: `[]` list: `T List` uall: `∀[x:A]. B[x]` member: `t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` face-cube: `cube(f)` I-face: `I-face(X;I)` pi2: `snd(t)` face-dimension: `dimension(f)` pi1: `fst(t)`
Lemmas referenced :  I-face_wf list_wf coordinate_name_wf cubical-set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution productElimination thin hypothesisEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry lemma_by_obid isectElimination isect_memberEquality because_Cache

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[I:Cname  List].  \mforall{}[f:I-face(X;I)].    (cube(f)  \mmember{}  X(I-[dimension(f)]))

Date html generated: 2016_06_16-PM-05_48_57
Last ObjectModification: 2015_12_28-PM-04_31_27

Theory : cubical!sets

Home Index