Nuprl Lemma : lower-rc-face-is-face

k:ℕ. ∀c:ℚCube(k). ∀j:ℕk.  lower-rc-face(c;j) ≤ c


Proof




Definitions occuring in Statement :  lower-rc-face: lower-rc-face(c;j) rat-cube-face: c ≤ d rational-cube: Cube(k) int_seg: {i..j-} nat: all: x:A. B[x] natural_number: $n
Definitions unfolded in proof :  nat: false: False assert: b bnot: ¬bb guard: {T} sq_type: SQType(T) exists: x:A. B[x] bfalse: ff or: P ∨ Q rat-interval-face: I ≤ J ifthenelse: if then else fi  uimplies: supposing a and: P ∧ Q uiff: uiff(P;Q) btrue: tt it: unit: Unit bool: 𝔹 int_seg: {i..j-} uall: [x:A]. B[x] pi1: fst(t) rational-interval: Interval implies:  Q rational-cube: Cube(k) member: t ∈ T lower-rc-face: lower-rc-face(c;j) rat-cube-face: c ≤ d all: x:A. B[x]
Lemmas referenced :  istype-nat rational-cube_wf int_seg_wf neg_assert_of_eq_int assert-bnot bool_subtype_base bool_wf subtype_base_sq bool_cases_sqequal eqff_to_assert rat-point-interval_wf assert_of_eq_int eqtt_to_assert eq_int_wf
Rules used in proof :  natural_numberEquality universeIsType inrFormation_alt voidElimination independent_functionElimination cumulativity instantiate dependent_functionElimination promote_hyp dependent_pairFormation_alt because_Cache equalityIstype unionIsType inlFormation_alt independent_isectElimination equalitySymmetry equalityTransitivity equalityElimination unionElimination rename setElimination isectElimination extract_by_obid introduction productElimination thin hypothesis inhabitedIsType hypothesisEquality sqequalHypSubstitution applyEquality cut sqequalRule lambdaFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}c:\mBbbQ{}Cube(k).  \mforall{}j:\mBbbN{}k.    lower-rc-face(c;j)  \mleq{}  c



Date html generated: 2019_10_29-AM-07_56_08
Last ObjectModification: 2019_10_17-PM-03_06_11

Theory : rationals


Home Index