Nuprl Lemma : sqequaln_sqlen

[a,b:Base]. ∀[n:ℕ].  (a ~n b) supposing ((a ≤b) and (b ≤a))


Definitions occuring in Statement :  nat: uimplies: supposing a uall: [x:A]. B[x] base: Base sqle_n: s ≤t sqequal_n: ~n t
Definitions unfolded in proof :  member: t ∈ T uimplies: 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

\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