Nuprl Lemma : stable__le

[i,j:ℤ].  Stable{i ≤ j}


Proof




Definitions occuring in Statement :  stable: Stable{P} uall: [x:A]. B[x] le: A ≤ B int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T implies:  Q all: x:A. B[x] stable: Stable{P} uimplies: supposing a le: A ≤ B and: P ∧ Q
Lemmas referenced :  stable__from_decidable le_wf decidable__le le_witness_for_triv istype-int
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_functionElimination dependent_functionElimination sqequalRule Error :isect_memberEquality_alt,  productElimination independent_isectElimination Error :isectIsTypeImplies,  Error :inhabitedIsType

Latex:
\mforall{}[i,j:\mBbbZ{}].    Stable\{i  \mleq{}  j\}



Date html generated: 2019_06_20-AM-11_26_28
Last ObjectModification: 2018_12_06-AM-10_48_30

Theory : arithmetic


Home Index