### Nuprl Lemma : sq_stable__ex_int_seg_ap

`∀n,m:ℤ. ∀f:{n..m-} ⟶ 𝔹.  SqStable(∃k:{n..m-}. (↑(f k)))`

Proof

Definitions occuring in Statement :  int_seg: `{i..j-}` assert: `↑b` bool: `𝔹` sq_stable: `SqStable(P)` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` apply: `f a` function: `x:A ⟶ B[x]` int: `ℤ`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` so_apply: `x[s]` implies: `P `` Q`
Lemmas referenced :  sq_stable_from_decidable exists_wf int_seg_wf assert_wf decidable__exists_int_seg decidable__assert bool_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis sqequalRule lambdaEquality applyEquality independent_functionElimination instantiate dependent_functionElimination functionEquality intEquality

Latex:
\mforall{}n,m:\mBbbZ{}.  \mforall{}f:\{n..m\msupminus{}\}  {}\mrightarrow{}  \mBbbB{}.    SqStable(\mexists{}k:\{n..m\msupminus{}\}.  (\muparrow{}(f  k)))

Date html generated: 2016_05_14-AM-07_29_18
Last ObjectModification: 2015_12_26-PM-01_26_50

Theory : int_2

Home Index