Nuprl Lemma : rng_of_alg_wf

A:Type. ∀a:algebra_sig{i:l}(A).  (a↓rg ∈ RngSig)


Proof




Definitions occuring in Statement :  rng_of_alg: a↓rg algebra_sig: algebra_sig{i:l}(A) all: x:A. B[x] member: t ∈ T universe: Type rng_sig: RngSig
Definitions unfolded in proof :  rng_of_alg: a↓rg rng_sig: RngSig all: x:A. B[x] member: t ∈ T
Lemmas referenced :  alg_car_wf alg_eq_wf alg_le_wf alg_plus_wf alg_zero_wf alg_minus_wf alg_times_wf alg_one_wf alg_div_wf unit_wf2 bool_wf algebra_sig_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep lambdaFormation cut dependent_pairEquality lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin cumulativity hypothesisEquality hypothesis because_Cache functionEquality unionEquality productEquality universeEquality

Latex:
\mforall{}A:Type.  \mforall{}a:algebra\_sig\{i:l\}(A).    (a\mdownarrow{}rg  \mmember{}  RngSig)



Date html generated: 2016_05_16-AM-07_26_19
Last ObjectModification: 2015_12_28-PM-05_08_20

Theory : algebras_1


Home Index