Nuprl Lemma : oset_of_ocmon_wf
∀[g:OMon]. (g↓oset ∈ LOSet)
Proof
Definitions occuring in Statement : 
oset_of_ocmon: g↓oset
, 
omon: OMon
, 
loset: LOSet
, 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
all: ∀x:A. B[x]
, 
omon: OMon
, 
and: P ∧ Q
, 
abmonoid: AbMon
, 
mon: Mon
, 
ulinorder: UniformLinorder(T;x,y.R[x; y])
, 
monoid_p: IsMonoid(T;op;id)
, 
uorder: UniformOrder(T;x,y.R[x; y])
, 
loset: LOSet
, 
poset: POSet{i}
, 
qoset: QOSet
, 
dset: DSet
, 
oset_of_ocmon: g↓oset
, 
dset_of_mon: g↓set
, 
set_car: |p|
, 
pi1: fst(t)
, 
set_eq: =b
, 
pi2: snd(t)
, 
prop: ℙ
, 
set_leq: a ≤ b
, 
set_le: ≤b
, 
so_lambda: λ2x y.t[x; y]
, 
so_apply: x[s1;s2]
, 
upreorder: UniformPreorder(T;x,y.R[x; y])
Lemmas referenced : 
omon_properties, 
abmonoid_properties, 
mon_properties, 
omon_wf, 
oset_of_ocmon_wf0, 
eqfun_p_wf, 
set_car_wf, 
set_eq_wf, 
upreorder_wf, 
set_leq_wf, 
uanti_sym_wf, 
connex_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation, 
introduction, 
cut, 
hypothesisEquality, 
sqequalHypSubstitution, 
extract_by_obid, 
dependent_functionElimination, 
thin, 
hypothesis, 
applyLambdaEquality, 
productElimination, 
setElimination, 
rename, 
isectElimination, 
equalityTransitivity, 
equalitySymmetry, 
sqequalRule, 
axiomEquality, 
dependent_set_memberEquality, 
lambdaEquality, 
because_Cache, 
independent_pairFormation
Latex:
\mforall{}[g:OMon].  (g\mdownarrow{}oset  \mmember{}  LOSet)
Date html generated:
2017_10_01-AM-08_14_35
Last ObjectModification:
2017_02_28-PM-01_58_48
Theory : groups_1
Home
Index