Nuprl Lemma : rng_times_wf

[r:RngSig]. (* ∈ |r| ⟶ |r| ⟶ |r|)


Proof




Definitions occuring in Statement :  rng_times: * rng_car: |r| rng_sig: RngSig uall: [x:A]. B[x] member: t ∈ T function: x:A ⟶ B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T rng_sig: RngSig rng_times: * rng_car: |r| pi1: fst(t) pi2: snd(t)
Lemmas referenced :  rng_sig_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin sqequalRule hypothesisEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry lemma_by_obid

Latex:
\mforall{}[r:RngSig].  (*  \mmember{}  |r|  {}\mrightarrow{}  |r|  {}\mrightarrow{}  |r|)



Date html generated: 2016_05_15-PM-00_20_13
Last ObjectModification: 2015_12_27-AM-00_03_01

Theory : rings_1


Home Index