Nuprl Lemma : int_iseg_wf

[i,j:ℤ].  ({i...j} ∈ Type)


Proof




Definitions occuring in Statement :  int_iseg: {i...j} uall: [x:A]. B[x] member: t ∈ T int: universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T int_iseg: {i...j} and: P ∧ Q prop:
Lemmas referenced :  le_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalRule setEquality intEquality productEquality extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry Error :inhabitedIsType,  isect_memberEquality Error :universeIsType

Latex:
\mforall{}[i,j:\mBbbZ{}].    (\{i...j\}  \mmember{}  Type)



Date html generated: 2019_06_20-AM-11_33_17
Last ObjectModification: 2018_09_26-AM-11_48_23

Theory : int_1


Home Index