Nuprl Lemma : sqequaln_sqlen
∀[a,b:Base]. ∀[n:ℕ]. (a ~n b) supposing ((a ≤n b) and (b ≤n a))
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,
sqle_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,
sqequalnSqlen
Latex:
\mforall{}[a,b:Base]. \mforall{}[n:\mBbbN{}]. (a \msim{}n b) supposing ((a \mleq{}n b) and (b \mleq{}n a))
Date html generated:
2019_06_20-AM-11_33_49
Last ObjectModification:
2018_10_16-PM-03_55_09
Theory : int_1
Home
Index