Nuprl Lemma : ss-prod-prod
∀[X,Y,Z:SeparationSpace]. ss-homeo(X × Y × Z;X × Y × Z)
Proof
Definitions occuring in Statement :
ss-homeo: ss-homeo(X;Y),
prod-ss: ss1 × ss2,
separation-space: SeparationSpace,
uall: ∀[x:A]. B[x]
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
top: Top,
ss-function: ss-function(X;Y;f),
all: ∀x:A. B[x],
implies: P ⇒ Q,
uiff: uiff(P;Q),
and: P ∧ Q,
uimplies: b supposing a,
subtype_rel: A ⊆r B,
ss-point: Point(ss),
record-select: r.x,
prod-ss: ss1 × ss2,
mk-ss: Point=P #=Sep cotrans=C,
record-update: r[x := v],
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
bfalse: ff,
btrue: tt,
rev_uimplies: rev_uimplies(P;Q),
pi1: fst(t),
pi2: snd(t),
cand: A c∧ B,
rev_implies: P ⇐ Q,
so_lambda: λ2x.t[x],
so_apply: x[s],
prop: ℙ,
iff: P ⇐⇒ Q,
ss-homeo: ss-homeo(X;Y),
exists: ∃x:A. B[x],
ss-ap: f(x),
ss-eq: x ≡ y,
not: ¬A,
false: False
Lemmas referenced :
ss-fun-point,
prod-ss-point,
ss-point_wf,
prod-ss-eq,
prod-ss_wf,
subtype_rel_self,
iff_weakening_uiff,
ss-eq_wf,
pi2_wf,
pi1_wf_top,
subtype_rel_product,
top_wf,
ss-function_wf,
separation-space_wf,
ss-sep_wf,
ss-ap_wf,
all_wf,
exists_wf,
ss-fun_wf,
ss-eq_weakening,
iff_transitivity
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
cut,
sqequalRule,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
isect_memberEquality,
voidElimination,
voidEquality,
hypothesis,
because_Cache,
dependent_set_memberEquality,
lambdaEquality,
spreadEquality,
hypothesisEquality,
independent_pairEquality,
productEquality,
lambdaFormation,
productElimination,
independent_isectElimination,
applyEquality,
independent_pairFormation,
promote_hyp,
dependent_pairEquality,
independent_functionElimination,
functionEquality,
dependent_pairFormation,
equalityTransitivity,
equalitySymmetry,
dependent_functionElimination
Latex:
\mforall{}[X,Y,Z:SeparationSpace]. ss-homeo(X \mtimes{} Y \mtimes{} Z;X \mtimes{} Y \mtimes{} Z)
Date html generated:
2020_05_20-PM-01_20_05
Last ObjectModification:
2018_08_31-AM-00_26_59
Theory : intuitionistic!topology
Home
Index