Nuprl Lemma : algebra_subtype_module
∀A:RngSig. (algebra{i:l}(A) ⊆r A-Module)
Proof
Definitions occuring in Statement : 
algebra: algebra{i:l}(A)
, 
module: A-Module
, 
subtype_rel: A ⊆r B
, 
all: ∀x:A. B[x]
, 
rng_sig: RngSig
Definitions unfolded in proof : 
all: ∀x:A. B[x]
, 
subtype_rel: A ⊆r B
, 
member: t ∈ T
, 
algebra: algebra{i:l}(A)
Lemmas referenced : 
algebra_wf, 
rng_sig_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
lambdaFormation, 
lambdaEquality, 
sqequalHypSubstitution, 
setElimination, 
thin, 
rename, 
hypothesisEquality, 
cut, 
lemma_by_obid, 
dependent_functionElimination, 
hypothesis
Latex:
\mforall{}A:RngSig.  (algebra\{i:l\}(A)  \msubseteq{}r  A-Module)
Date html generated:
2016_05_16-AM-07_27_25
Last ObjectModification:
2015_12_28-PM-05_07_33
Theory : algebras_1
Home
Index