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