Nuprl Lemma : permutation-ss-point
∀[rv:Top]
(Point ~ {fg:Point ⟶ Point × (Point ⟶ Point)|
let f,g = fg
in (∀x:Point. f (g x) ≡ x)
∧ (∀x:Point. g (f x) ≡ x)
∧ (∀x,y:Point. (f x # f y
⇒ x # y))
∧ (∀x,y:Point. (g x # g y
⇒ x # y))} )
Proof
Definitions occuring in Statement :
permutation-ss: permutation-ss(ss)
,
ss-eq: x ≡ y
,
ss-sep: x # y
,
ss-point: Point
,
uall: ∀[x:A]. B[x]
,
top: Top
,
all: ∀x:A. B[x]
,
implies: P
⇒ Q
,
and: P ∧ Q
,
set: {x:A| B[x]}
,
apply: f a
,
function: x:A ⟶ B[x]
,
spread: spread def,
product: x:A × B[x]
,
sqequal: s ~ t
Definitions unfolded in proof :
fun-ss: A ⟶ ss
,
prod-ss: ss1 × ss2
,
uall: ∀[x:A]. B[x]
,
btrue: tt
,
bfalse: ff
,
ifthenelse: if b then t else f fi
,
eq_atom: x =a y
,
top: Top
,
member: t ∈ T
,
all: ∀x:A. B[x]
,
mk-ss: mk-ss,
set-ss: set-ss(ss;x.P[x])
,
permutation-ss: permutation-ss(ss)
,
ss-point: Point
Lemmas referenced :
top_wf,
rec_select_update_lemma
Rules used in proof :
sqequalAxiom,
isect_memberFormation,
hypothesis,
voidEquality,
voidElimination,
isect_memberEquality,
thin,
dependent_functionElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
computationStep,
sqequalTransitivity,
sqequalReflexivity,
sqequalRule,
sqequalSubstitution
Latex:
\mforall{}[rv:Top]
(Point \msim{} \{fg:Point {}\mrightarrow{} Point \mtimes{} (Point {}\mrightarrow{} Point)|
let f,g = fg
in (\mforall{}x:Point. f (g x) \mequiv{} x)
\mwedge{} (\mforall{}x:Point. g (f x) \mequiv{} x)
\mwedge{} (\mforall{}x,y:Point. (f x \# f y {}\mRightarrow{} x \# y))
\mwedge{} (\mforall{}x,y:Point. (g x \# g y {}\mRightarrow{} x \# y))\} )
Date html generated:
2016_11_08-AM-09_12_43
Last ObjectModification:
2016_11_03-AM-10_29_11
Theory : inner!product!spaces
Home
Index