Nuprl Lemma : respects-equality-oalist2
∀[s:LOSet]. ∀[g:AbDMon]. respects-equality((|s| × |g|) List;|oal(s;g)|)
Proof
Definitions occuring in Statement :
oalist: oal(a;b),
list: T List,
respects-equality: respects-equality(S;T),
uall: ∀[x:A]. B[x],
product: x:A × B[x],
abdmonoid: AbDMon,
grp_car: |g|,
loset: LOSet,
set_car: |p|
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
set_car: |p|,
pi1: fst(t),
set_prod: s × t,
mk_dset: mk_dset(T, eq),
grp_car: |g|,
dset_of_mon: g↓set
Lemmas referenced :
respects-equality-oalist1,
abdmonoid_wf,
loset_wf
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
sqequalRule,
universeIsType
Latex:
\mforall{}[s:LOSet]. \mforall{}[g:AbDMon]. respects-equality((|s| \mtimes{} |g|) List;|oal(s;g)|)
Date html generated:
2019_10_16-PM-01_07_04
Last ObjectModification:
2018_11_27-AM-11_23_17
Theory : polynom_2
Home
Index