Nuprl Lemma : sqlen_sqequaln
∀[a,b:Base]. ∀[n:ℕ]. a ≤n b supposing a ~n b
Proof
Definitions occuring in Statement :
nat: ℕ,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
base: Base,
sqle_n: s ≤n t,
sqequal_n: s ~n t
Definitions unfolded in proof :
member: t ∈ T,
uimplies: b supposing a,
uall: ∀[x:A]. B[x]
Lemmas referenced :
base_wf,
nat_wf,
sqequal_n_wf
Rules used in proof :
Error :inhabitedIsType,
hypothesis,
hypothesisEquality,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
Error :universeIsType,
Error :isect_memberFormation_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
sqlenSqequaln
Latex:
\mforall{}[a,b:Base]. \mforall{}[n:\mBbbN{}]. a \mleq{}n b supposing a \msim{}n b
Date html generated:
2019_06_20-AM-11_33_51
Last ObjectModification:
2018_10_16-PM-02_52_22
Theory : int_1
Home
Index