Nuprl Lemma : subtype-orthogonal-group
∀[rv:InnerProductSpace]
({fg:Point ⟶ Point × (Point ⟶ Point)| let f,g = fg in (∀x:Point. f (g x) ≡ x) ∧ Orthogonal(f)} ⊆r Point)
Proof
Definitions occuring in Statement :
orthogonal-group: O(rv),
rv-orthogonal: Orthogonal(f),
inner-product-space: InnerProductSpace,
ss-eq: x ≡ y,
ss-point: Point,
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
spread: spread def,
product: x:A × B[x]
Definitions unfolded in proof :
guard: {T},
pi1: fst(t),
so_apply: x[s],
so_lambda: λ2x.t[x],
prop: ℙ,
implies: P ⇒ Q,
uimplies: b supposing a,
cand: A c∧ B,
and: P ∧ Q,
btrue: tt,
mk-ss: mk-ss,
bfalse: ff,
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
top: Top,
all: ∀x:A. B[x],
mk-s-group: mk-s-group(ss; e; i; o; sep; invsep),
set-ss: set-ss(ss;x.P[x]),
mk-s-subgroup: mk-s-subgroup(sg;x.P[x]),
ss-point: Point,
orthogonal-group: O(rv),
subtype_rel: A ⊆r B,
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
separation-space_wf,
real-vector-space_wf,
inner-product-space_wf,
subtype_rel_transitivity,
inner-product-space_subtype,
real-vector-space_subtype1,
top_wf,
subtype_rel_product,
pi1_wf_top,
rv-orthogonal_wf,
ss-eq_wf,
all_wf,
ss-sep_wf,
rv-orthogonal-injective,
rv-orthogonal-implies-extensional,
rv-orthogonal-inverse,
ss-point_wf,
rv-perm-point,
rec_select_update_lemma
Rules used in proof :
axiomEquality,
instantiate,
setEquality,
functionEquality,
productEquality,
independent_functionElimination,
independent_isectElimination,
lambdaFormation,
independent_pairFormation,
because_Cache,
hypothesisEquality,
applyEquality,
functionExtensionality,
independent_pairEquality,
dependent_set_memberEquality,
isectElimination,
hypothesis,
voidEquality,
voidElimination,
isect_memberEquality,
dependent_functionElimination,
extract_by_obid,
sqequalRule,
sqequalHypSubstitution,
productElimination,
rename,
thin,
setElimination,
lambdaEquality,
cut,
introduction,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[rv:InnerProductSpace]
(\{fg:Point {}\mrightarrow{} Point \mtimes{} (Point {}\mrightarrow{} Point)| let f,g = fg in (\mforall{}x:Point. f (g x) \mequiv{} x) \mwedge{} Orthogonal(f)\}
\msubseteq{}r Point)
Date html generated:
2016_11_08-AM-09_21_23
Last ObjectModification:
2016_11_03-PM-00_11_44
Theory : inner!product!spaces
Home
Index