Step
*
of Lemma
rv-orthog-ext_wf
∀rv:InnerProductSpace. ∀f:Point ⟶ Point.
rv-orthog-ext(rv;f) ∈ ∀x,y:Point. (f x # f y
⇒ x # y) supposing Orthogonal(f)
BY
{ (Auto
THEN (Assert TERMOF{rv-orthogonal-implies-extensional-ext:o, 1:l, i:l} rv f ∈ ∀x,y:Point. (f x # f y
⇒ x # y) BY
Auto)
) }
1
1. rv : InnerProductSpace
2. f : Point ⟶ Point
3. Orthogonal(f)
4. TERMOF{rv-orthogonal-implies-extensional-ext:o, 1:l, i:l} rv f ∈ ∀x,y:Point. (f x # f y
⇒ x # y)
⊢ rv-orthog-ext(rv;f) ∈ ∀x,y:Point. (f x # f y
⇒ x # y)
Latex:
Latex:
\mforall{}rv:InnerProductSpace. \mforall{}f:Point {}\mrightarrow{} Point.
rv-orthog-ext(rv;f) \mmember{} \mforall{}x,y:Point. (f x \# f y {}\mRightarrow{} x \# y) supposing Orthogonal(f)
By
Latex:
(Auto
THEN (Assert TERMOF\{rv-orthogonal-implies-extensional-ext:o, 1:l, i:l\} rv f \mmember{} \mforall{}x,y:Point.
(f x \# f y
{}\mRightarrow{} x \# y) BY
Auto)
)
Home
Index