Nuprl Lemma : ble_wf
∀[n,m:ℤ]. (ble(n;m) ∈ 𝔹)
Proof
Definitions occuring in Statement :
ble: ble(n;m),
bool: 𝔹,
uall: ∀[x:A]. B[x],
member: t ∈ T,
int: ℤ
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
ble: ble(n;m),
false: False,
implies: P ⇒ Q,
not: ¬A,
less_than: a < b,
and: P ∧ Q,
less_than': less_than'(a;b),
true: True,
squash: ↓T,
top: Top,
prop: ℙ
Lemmas referenced :
btrue_wf,
top_wf,
less_than_wf,
bfalse_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalRule,
int_eqEquality,
hypothesisEquality,
extract_by_obid,
hypothesis,
sqequalHypSubstitution,
lessCases,
independent_pairFormation,
isectElimination,
thin,
baseClosed,
natural_numberEquality,
equalityTransitivity,
equalitySymmetry,
imageMemberEquality,
axiomSqEquality,
isect_memberEquality,
because_Cache,
voidElimination,
voidEquality,
lambdaFormation,
imageElimination,
productElimination,
independent_functionElimination,
axiomEquality,
intEquality
Latex:
\mforall{}[n,m:\mBbbZ{}]. (ble(n;m) \mmember{} \mBbbB{})
Date html generated:
2019_06_20-PM-03_03_12
Last ObjectModification:
2018_08_20-PM-09_40_40
Theory : continuity
Home
Index