Nuprl Lemma : int_le_to_int_upper

i:ℤ. ∀[A:{i...} ⟶ ℙ]. ({∀j:ℤA[j] supposing i ≤ j} ⇐⇒ {∀j:{i...}. A[j]})


Proof




Definitions occuring in Statement :  int_upper: {i...} uimplies: supposing a uall: [x:A]. B[x] prop: guard: {T} so_apply: x[s] le: A ≤ B all: x:A. B[x] iff: ⇐⇒ Q function: x:A ⟶ B[x] int:
Definitions unfolded in proof :  guard: {T} all: x:A. B[x] uall: [x:A]. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q member: t ∈ T int_upper: {i...} uimplies: supposing a sq_stable: SqStable(P) squash: T prop: so_lambda: λ2x.t[x] so_apply: x[s] rev_implies:  Q le: A ≤ B not: ¬A false: False
Lemmas referenced :  less_than'_wf le_wf isect_wf all_wf int_upper_wf sq_stable__le
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep lambdaFormation isect_memberFormation independent_pairFormation cut hypothesis sqequalHypSubstitution dependent_functionElimination thin setElimination rename hypothesisEquality independent_isectElimination lemma_by_obid isectElimination independent_functionElimination introduction imageMemberEquality baseClosed imageElimination intEquality lambdaEquality applyEquality dependent_set_memberEquality because_Cache productElimination independent_pairEquality voidElimination axiomEquality functionEquality cumulativity universeEquality

Latex:
\mforall{}i:\mBbbZ{}.  \mforall{}[A:\{i...\}  {}\mrightarrow{}  \mBbbP{}].  (\{\mforall{}j:\mBbbZ{}.  A[j]  supposing  i  \mleq{}  j\}  \mLeftarrow{}{}\mRightarrow{}  \{\mforall{}j:\{i...\}.  A[j]\})



Date html generated: 2016_05_13-PM-04_02_43
Last ObjectModification: 2016_01_14-PM-07_24_31

Theory : int_1


Home Index