Step
*
1
of Lemma
mk-inner-product-space_wf
1. self : self:SeparationSpace
"0":Point(self)
"+":{f:Point(self) ⟶ Point(self) ⟶ Point(self)|
(∀x,y,z:Point(self). f x (f y z) ≡ f (f x y) z) ∧ (∀x,y:Point(self). f x y ≡ f y x)}
"+sep":∀x,x',y,y':Point(self). (self."+" x y # self."+" x' y' ⇒ (x # x' ∨ y # y'))
"*":{m:ℝ ⟶ Point(self) ⟶ Point(self)|
(∀a:ℝ. ∀x,y:Point(self). m a (self."+" x y) ≡ self."+" (m a x) (m a y))
∧ (∀x:Point(self)
(m r1 x ≡ x
∧ m r0 x ≡ self."0"
∧ (∀a,b:ℝ. m a (m b x) ≡ m (a * b) x)
∧ (∀a,b:ℝ. m (a + b) x ≡ self."+" (m a x) (m b x))))} ⋂ x:Atom ⟶ if x =a "*sep"
then ∀a,b:ℝ. ∀x,y:Point(self).
(self."*" a x # self."*" b y
⇒ (a ≠ b ∨ x # y))
else Top
fi
2. self ∈ SeparationSpace
3. ip : {ip:Point(self) ⟶ Point(self) ⟶ ℝ|
(∀x1,x2,y1,y2:Point(self). (x1 ≡ x2 ⇒ y1 ≡ y2 ⇒ ((ip x1 y1) = (ip x2 y2))))
∧ (∀x,y:Point(self). ((ip x y) = (ip y x)))
∧ (∀x,y,z:Point(self). ((ip x + y z) = ((ip x z) + (ip y z))))
∧ (∀a:ℝ. ∀x,y:Point(self). ((ip a*x y) = (a * (ip x y))))}
4. pos : ∀x:Point(self). (x # 0 ⇐⇒ r0 < (ip x x))
5. perp : ∀x:Point(self). (x # 0 ⇒ (∃y:Point(self). (y # 0 ∧ ((ip x y) = r0))))
6. self ∈ RealVectorSpace
7. self."0" ∈ Point(self)
8. self."+" ∈ {f:Point(self) ⟶ Point(self) ⟶ Point(self)|
(∀x,y,z:Point(self). f x (f y z) ≡ f (f x y) z) ∧ (∀x,y:Point(self). f x y ≡ f y x)}
9. self."+sep" ∈ ∀x,x',y,y':Point(self). (self."+" x y # self."+" x' y' ⇒ (x # x' ∨ y # y'))
10. self."*" ∈ {m:ℝ ⟶ Point(self) ⟶ Point(self)|
(∀a:ℝ. ∀x,y:Point(self). m a (self."+" x y) ≡ self."+" (m a x) (m a y))
∧ (∀x:Point(self)
(m r1 x ≡ x
∧ m r0 x ≡ self."0"
∧ (∀a,b:ℝ. m a (m b x) ≡ m (a * b) x)
∧ (∀a,b:ℝ. m (a + b) x ≡ self."+" (m a x) (m b x))))}
11. self."*sep" ∈ ∀a,b:ℝ. ∀x,y:Point(self). (self."*" a x # self."*" b y ⇒ (a ≠ b ∨ x # y))
⊢ self["ip" := ip]["positive" := pos]["perp" := perp] ∈ SeparationSpace
BY
{ ((GenConcl ⌜self = ss ∈ SeparationSpace⌝⋅ THENA Auto)
THEN (GenConcl ⌜ip = xx ∈ Top⌝⋅ THENA Auto)
THEN (GenConcl ⌜pos = xxx ∈ Top⌝⋅ THENA Auto)
THEN (GenConcl ⌜perp = xxxx ∈ Top⌝⋅ THENA Auto)
THEN All Thin
THEN ((D 1 THENA Auto) THEN Unfold `separation-space` 0)
THEN RepeatFor 3 ((RecordPlusTypeCD THENL [ Id; (Reduce 0 THEN Trivial)]))) }
1
1. ss : self:"Point":Type
"#":{s:self."Point" ⟶ self."Point" ⟶ ℙ| ∀x:self."Point". (¬(s x x))} ⋂ x:Atom ⟶ if x =a "#or"
then ∀x,y,z:self."Point".
((self."#" x y)
⇒ ((self."#" x z)
∨ (self."#" y z)))
else Top
fi
2. ss ∈ record(x.Top)
3. xx : Top
4. xxx : Top
5. xxxx : Top
6. ss."Point" ∈ Type
7. ss."#" ∈ {s:ss."Point" ⟶ ss."Point" ⟶ ℙ| ∀x:ss."Point". (¬(s x x))}
8. ss."#or" ∈ ∀x,y,z:ss."Point". ((ss."#" x y) ⇒ ((ss."#" x z) ∨ (ss."#" y z)))
⊢ ss["ip" := xx]["positive" := xxx]["perp" := xxxx] ∈ record(x.Top)
Latex:
Latex:
1. self : self:SeparationSpace
"0":Point(self)
"+":\{f:Point(self) {}\mrightarrow{} Point(self) {}\mrightarrow{} Point(self)|
(\mforall{}x,y,z:Point(self). f x (f y z) \mequiv{} f (f x y) z)
\mwedge{} (\mforall{}x,y:Point(self). f x y \mequiv{} f y x)\}
"+sep":\mforall{}x,x',y,y':Point(self). (self."+" x y \# self."+" x' y' {}\mRightarrow{} (x \# x' \mvee{} y \# y'))
"*":\{m:\mBbbR{} {}\mrightarrow{} Point(self) {}\mrightarrow{} Point(self)|
(\mforall{}a:\mBbbR{}. \mforall{}x,y:Point(self). m a (self."+" x y) \mequiv{} self."+" (m a x) (m a y))
\mwedge{} (\mforall{}x:Point(self)
(m r1 x \mequiv{} x
\mwedge{} m r0 x \mequiv{} self."0"
\mwedge{} (\mforall{}a,b:\mBbbR{}. m a (m b x) \mequiv{} m (a * b) x)
\mwedge{} (\mforall{}a,b:\mBbbR{}. m (a + b) x \mequiv{} self."+" (m a x) (m b x))))\} \mcap{} x:Atom
{}\mrightarrow{} if x =a "*sep"
then \mforall{}a,b:\mBbbR{}. \mforall{}x,y:Point(self). (self."*" a x \# self."*" b y {}\mRightarrow{} (a \mneq{} b \mvee{} x \# y))
else Top
fi
2. self \mmember{} SeparationSpace
3. ip : \{ip:Point(self) {}\mrightarrow{} Point(self) {}\mrightarrow{} \mBbbR{}|
(\mforall{}x1,x2,y1,y2:Point(self). (x1 \mequiv{} x2 {}\mRightarrow{} y1 \mequiv{} y2 {}\mRightarrow{} ((ip x1 y1) = (ip x2 y2))))
\mwedge{} (\mforall{}x,y:Point(self). ((ip x y) = (ip y x)))
\mwedge{} (\mforall{}x,y,z:Point(self). ((ip x + y z) = ((ip x z) + (ip y z))))
\mwedge{} (\mforall{}a:\mBbbR{}. \mforall{}x,y:Point(self). ((ip a*x y) = (a * (ip x y))))\}
4. pos : \mforall{}x:Point(self). (x \# 0 \mLeftarrow{}{}\mRightarrow{} r0 < (ip x x))
5. perp : \mforall{}x:Point(self). (x \# 0 {}\mRightarrow{} (\mexists{}y:Point(self). (y \# 0 \mwedge{} ((ip x y) = r0))))
6. self \mmember{} RealVectorSpace
7. self."0" \mmember{} Point(self)
8. self."+" \mmember{} \{f:Point(self) {}\mrightarrow{} Point(self) {}\mrightarrow{} Point(self)|
(\mforall{}x,y,z:Point(self). f x (f y z) \mequiv{} f (f x y) z)
\mwedge{} (\mforall{}x,y:Point(self). f x y \mequiv{} f y x)\}
9. self."+sep" \mmember{} \mforall{}x,x',y,y':Point(self). (self."+" x y \# self."+" x' y' {}\mRightarrow{} (x \# x' \mvee{} y \# y'))
10. self."*" \mmember{} \{m:\mBbbR{} {}\mrightarrow{} Point(self) {}\mrightarrow{} Point(self)|
(\mforall{}a:\mBbbR{}. \mforall{}x,y:Point(self). m a (self."+" x y) \mequiv{} self."+" (m a x) (m a y))
\mwedge{} (\mforall{}x:Point(self)
(m r1 x \mequiv{} x
\mwedge{} m r0 x \mequiv{} self."0"
\mwedge{} (\mforall{}a,b:\mBbbR{}. m a (m b x) \mequiv{} m (a * b) x)
\mwedge{} (\mforall{}a,b:\mBbbR{}. m (a + b) x \mequiv{} self."+" (m a x) (m b x))))\}
11. self."*sep" \mmember{} \mforall{}a,b:\mBbbR{}. \mforall{}x,y:Point(self). (self."*" a x \# self."*" b y {}\mRightarrow{} (a \mneq{} b \mvee{} x \# y))
\mvdash{} self["ip" := ip]["positive" := pos]["perp" := perp] \mmember{} SeparationSpace
By
Latex:
((GenConcl \mkleeneopen{}self = ss\mkleeneclose{}\mcdot{} THENA Auto)
THEN (GenConcl \mkleeneopen{}ip = xx\mkleeneclose{}\mcdot{} THENA Auto)
THEN (GenConcl \mkleeneopen{}pos = xxx\mkleeneclose{}\mcdot{} THENA Auto)
THEN (GenConcl \mkleeneopen{}perp = xxxx\mkleeneclose{}\mcdot{} THENA Auto)
THEN All Thin
THEN ((D 1 THENA Auto) THEN Unfold `separation-space` 0)
THEN RepeatFor 3 ((RecordPlusTypeCD THENL [ Id; (Reduce 0 THEN Trivial)])))
Home
Index