Nuprl Lemma : le_int-wf-bar-int


[x,y:bar(ℤ)].  (x ≤y ∈ bar(𝔹))


Proof




Definitions occuring in Statement :  bar: bar(T) le_int: i ≤j bool: 𝔹 uall: [x:A]. B[x] member: t ∈ T int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a and: P ∧ Q cand: c∧ B guard: {T} or: P ∨ Q subtype_rel: A ⊆B all: x:A. B[x] implies:  Q
Lemmas referenced :  subtype_bar2 base_wf int_subtype_base value-type_wf subtype_rel_self bar-base le_int-wf-bar subtype_barSqtype_base int-value-type
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin intEquality hypothesis independent_isectElimination independent_pairFormation sqequalRule inrFormation because_Cache hypothesisEquality applyEquality dependent_functionElimination independent_functionElimination axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

Latex:
\mforall{}[x,y:bar(\mBbbZ{})].    (x  \mleq{}z  y  \mmember{}  bar(\mBbbB{}))



Date html generated: 2016_07_08-PM-05_18_57
Last ObjectModification: 2015_12_27-PM-05_17_05

Theory : bar!type


Home Index