Nuprl Lemma : fills-open_box_wf

[X:CubicalSet]. ∀[I,J:Cname List]. ∀[x:nameset(I)]. ∀[i:ℕ2].
  ∀[bx:open_box(X;I;J;x;i)]. ∀[cube:X(I)].  (fills-open_box(X;I;bx;cube) ∈ ℙsupposing l_subset(Cname;J;I)


Proof




Definitions occuring in Statement :  fills-open_box: fills-open_box(X;I;bx;cube) open_box: open_box(X;I;J;x;i) I-cube: X(I) cubical-set: CubicalSet nameset: nameset(L) coordinate_name: Cname l_subset: l_subset(T;as;bs) list: List int_seg: {i..j-} uimplies: supposing a uall: [x:A]. B[x] prop: member: t ∈ T natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a fills-open_box: fills-open_box(X;I;bx;cube) open_box: open_box(X;I;J;x;i) prop:
Lemmas referenced :  fills-faces_wf I-cube_wf open_box_wf l_subset_wf coordinate_name_wf int_seg_wf nameset_wf list_wf cubical-set_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality setElimination rename hypothesis axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache natural_numberEquality

Latex:
\mforall{}[X:CubicalSet].  \mforall{}[I,J:Cname  List].  \mforall{}[x:nameset(I)].  \mforall{}[i:\mBbbN{}2].
    \mforall{}[bx:open\_box(X;I;J;x;i)].  \mforall{}[cube:X(I)].    (fills-open\_box(X;I;bx;cube)  \mmember{}  \mBbbP{}) 
    supposing  l\_subset(Cname;J;I)



Date html generated: 2016_06_16-PM-06_42_57
Last ObjectModification: 2015_12_28-PM-04_26_16

Theory : cubical!sets


Home Index