Nuprl Lemma : ob_product_lemma
∀B,A:Top. (cat-ob(A × B) ~ cat-ob(A) × cat-ob(B))
Proof
Definitions occuring in Statement :
product-cat: A × B,
cat-ob: cat-ob(C),
top: Top,
all: ∀x:A. B[x],
product: x:A × B[x],
sqequal: s ~ t
Definitions unfolded in proof :
all: ∀x:A. B[x],
cat-ob: cat-ob(C),
product-cat: A × B,
pi1: fst(t),
member: t ∈ T
Lemmas referenced :
top_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
sqequalRule,
hypothesis,
introduction,
extract_by_obid
Latex:
\mforall{}B,A:Top. (cat-ob(A \mtimes{} B) \msim{} cat-ob(A) \mtimes{} cat-ob(B))
Date html generated:
2020_05_20-AM-07_54_05
Last ObjectModification:
2017_01_09-PM-00_36_03
Theory : small!categories
Home
Index