Nuprl Lemma : cube-face_wf

[k:ℕ]. ∀[i:ℕk]. ∀[up:𝔹]. ∀[c:real-cube(k)].  (cube-face(i;up;c) ∈ real-cube(k))


Proof




Definitions occuring in Statement :  cube-face: cube-face(i;up;c) real-cube: real-cube(k) int_seg: {i..j-} nat: bool: 𝔹 uall: [x:A]. B[x] member: t ∈ T natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T real-cube: real-cube(k) bool: 𝔹 unit: Unit it: btrue: tt cube-face: cube-face(i;up;c) ifthenelse: if then else fi  real-vec: ^n int_seg: {i..j-} bfalse: ff nat:
Lemmas referenced :  ifthenelse_wf eq_int_wf real_wf real-cube_wf bool_wf int_seg_wf istype-nat
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalHypSubstitution productElimination thin unionElimination equalityElimination sqequalRule independent_pairEquality lambdaEquality_alt extract_by_obid isectElimination setElimination rename hypothesisEquality hypothesis applyEquality inhabitedIsType because_Cache axiomEquality equalityTransitivity equalitySymmetry universeIsType isect_memberEquality_alt isectIsTypeImplies natural_numberEquality

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[i:\mBbbN{}k].  \mforall{}[up:\mBbbB{}].  \mforall{}[c:real-cube(k)].    (cube-face(i;up;c)  \mmember{}  real-cube(k))



Date html generated: 2019_10_30-AM-11_32_01
Last ObjectModification: 2019_09_27-PM-01_49_52

Theory : real!vectors


Home Index