### Nuprl Lemma : int_seg_well_founded_up

`∀i:ℤ. ∀j:{i...}.  WellFnd{i}({i..j-};x,y.x < y)`

Proof

Definitions occuring in Statement :  int_upper: `{i...}` int_seg: `{i..j-}` wellfounded: `WellFnd{i}(A;x,y.R[x; y])` less_than: `a < b` all: `∀x:A. B[x]` int: `ℤ`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` so_lambda: `λ2x y.t[x; y]` int_upper: `{i...}` so_apply: `x[s1;s2]` subtype_rel: `A ⊆r B` uimplies: `b supposing a` implies: `P `` Q`
Lemmas referenced :  int_upper_wf istype-int int_upper_well_founded inv_image_ind less_than_wf int_seg_wf int_seg_subtype_upper le_reflexive
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  Error :universeIsType,  cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis dependent_functionElimination sqequalRule Error :lambdaEquality_alt,  setElimination rename because_Cache Error :inhabitedIsType,  applyEquality independent_isectElimination independent_functionElimination

Latex:
\mforall{}i:\mBbbZ{}.  \mforall{}j:\{i...\}.    WellFnd\{i\}(\{i..j\msupminus{}\};x,y.x  <  y)

Date html generated: 2019_06_20-PM-01_15_21
Last ObjectModification: 2018_10_03-PM-10_11_28

Theory : int_2

Home Index