Nuprl Lemma : oal_hgp_subtype_oal_grp
∀s:LOSet. ∀g:OGrp. (|oal_hgp(s;g)| ⊆r |oal_grp(s;g)|)
Proof
Definitions occuring in Statement :
oal_hgp: oal_hgp(s;g),
oal_grp: oal_grp(s;g),
subtype_rel: A ⊆r B,
all: ∀x:A. B[x],
ocgrp: OGrp,
grp_car: |g|,
loset: LOSet
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
oal_grp: oal_grp(s;g),
grp_car: |g|,
oal_hgp: oal_hgp(s;g),
pi1: fst(t)
Lemmas referenced :
ocgrp_wf,
loset_wf,
set_car_inc
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
lemma_by_obid,
hypothesis,
sqequalRule,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality
Latex:
\mforall{}s:LOSet. \mforall{}g:OGrp. (|oal\_hgp(s;g)| \msubseteq{}r |oal\_grp(s;g)|)
Date html generated:
2016_05_16-AM-08_22_25
Last ObjectModification:
2015_12_28-PM-06_24_51
Theory : polynom_2
Home
Index