Nuprl Lemma : algebra_wf

A:RngSig. (algebra{i:l}(A) ∈ 𝕌')


Proof




Definitions occuring in Statement :  algebra: algebra{i:l}(A) all: x:A. B[x] member: t ∈ T universe: Type rng_sig: RngSig
Definitions unfolded in proof :  algebra: algebra{i:l}(A) all: x:A. B[x] member: t ∈ T and: P ∧ Q uall: [x:A]. B[x] module: A-Module subtype_rel: A ⊆B prop: so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  module_wf monoid_p_wf alg_car_wf rng_car_wf alg_times_wf alg_one_wf bilinear_wf alg_plus_wf all_wf dist_1op_2op_lr_wf alg_act_wf rng_sig_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep lambdaFormation cut setEquality lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality hypothesis productEquality isectElimination because_Cache setElimination rename applyEquality lambdaEquality cumulativity universeEquality

Latex:
\mforall{}A:RngSig.  (algebra\{i:l\}(A)  \mmember{}  \mBbbU{}')



Date html generated: 2016_05_16-AM-07_27_22
Last ObjectModification: 2015_12_28-PM-05_07_52

Theory : algebras_1


Home Index