### Nuprl Lemma : cube-set-restriction_wf

`∀[X:CubicalSet]. ∀[I,J:Cname List]. ∀[f:name-morph(I;J)]. ∀[s:X(I)].  (f(s) ∈ X(J))`

Proof

Definitions occuring in Statement :  cube-set-restriction: `f(s)` I-cube: `X(I)` cubical-set: `CubicalSet` name-morph: `name-morph(I;J)` coordinate_name: `Cname` list: `T List` uall: `∀[x:A]. B[x]` member: `t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` cube-set-restriction: `f(s)` cubical-set: `CubicalSet` pi2: `snd(t)` I-cube: `X(I)` functor-ob: `functor-ob(F)` pi1: `fst(t)`
Lemmas referenced :  I-cube_wf name-morph_wf list_wf coordinate_name_wf cubical-set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution setElimination thin rename productElimination applyEquality hypothesisEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry lemma_by_obid isectElimination isect_memberEquality because_Cache

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[I,J:Cname  List].  \mforall{}[f:name-morph(I;J)].  \mforall{}[s:X(I)].    (f(s)  \mmember{}  X(J))

Date html generated: 2016_06_16-PM-05_36_35
Last ObjectModification: 2015_12_28-PM-04_37_24

Theory : cubical!sets

Home Index