MyWikiBiz, Author Your Legacy — Wednesday November 05, 2025
Jump to navigationJump to search
703 bytes removed
, 04:10, 13 February 2009
| Line 4,250: |
Line 4,250: |
| | | | |
| | ===Fact 2.3=== | | ===Fact 2.3=== |
| − |
| |
| − | <pre>
| |
| − | Fact 2.3
| |
| − |
| |
| − | If R c OxSxI,
| |
| − |
| |
| − | then the following are equivalent:
| |
| − |
| |
| − | F2.3a. DerR = {<x, y> C SxI :
| |
| − | Conj(o C O)
| |
| − | {Den(R, x)}(o) =
| |
| − | {Den(R, y)}(o)
| |
| − | } :R11a
| |
| − | ::
| |
| − | F2.3b. {DerR} : SxI -> B
| |
| − | :
| |
| − | {DerR}(x, y) = [ Conj(o C O)
| |
| − | {Den(R, x)}(o) =
| |
| − | {Den(R, y)}(o)
| |
| − | ] :R11d
| |
| − | ::
| |
| − | F2.3c. {DerR}(x, y) = Conj(o C O)
| |
| − | [ {Den(R, x)}(o) =
| |
| − | {Den(R, y)}(o)
| |
| − | ] :Log
| |
| − | ::
| |
| − | F2.3d. {DerR}(x, y) = Conj(o C O)
| |
| − | [ {DenR}(o, x) =
| |
| − | {DenR}(o, y)
| |
| − | ] :Def
| |
| − | ::
| |
| − | F2.3e. {DerR}(x, y) = Conj(o C O)
| |
| − | (( {DenR}(o, x),
| |
| − | {DenR}(o, y)
| |
| − | )) :Log
| |
| − | :D10b
| |
| − | ::
| |
| − | F2.3f. {DerR}(x, y) = Conj(o C O)
| |
| − | (( {ROS}(o, x),
| |
| − | {ROS}(o, y)
| |
| − | )) :D10a
| |
| − | </pre>
| |
| | | | |
| | <br> | | <br> |
| Line 4,421: |
Line 4,379: |
| | |- style="height:100px" | | |- style="height:100px" |
| | | | | | |
| − | | valign="top" | <math>\operatorname{F2.2f.}</math> | + | | valign="top" | <math>\operatorname{F2.3f.}</math> |
| | | valign="top" | | | | valign="top" | |
| | <math>\begin{array}{ccccl} | | <math>\begin{array}{ccccl} |
