Home(or GIF version for IE).
| Home |
Metamath Proof Explorer | < Previous Next > |
| Bad symbols?
Use Firefox (or GIF version for IE). |
| Color key: | Metamath Proof Explorer
(1-9063) |
Hilbert Space Explorer
(9064-10651) |
Users' Mathboxes
(10652-12230) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Syntax | cla 8901 | Extend class notation with the class of all lattices. |
| class Lat | ||
| Definition | df-ps 8902 | Define the class of all posets (partially ordered sets) with weak ordering (e.g. "less than or equal to" instead of "less than"). A poset is a relation which is transitive, reflexive, and antisymmetric. |
| ⊢ Poset = {r∣(Rel r ⋀ (r ∘ r) ⊆ r ⋀ (r ∩ ◡r) = (I ↾ ∪∪r))} | ||
| Definition | df-spw 8903 | Define suprema under weak orderings. Unlike df-sup 4718 for strong orderings, supw is evaluates to a member of the field of R iff the supremum exists. Read R supw A as the R -supremum of set A. |
⊢ supw = { r,
x , y∣∃z(z = {w ∈ ∪∪r∣(∀v ∈ x vrw ⋀ ∀v ∈ ∪∪r(∀u ∈ x urv → wrv))} ⋀ y = if(z ≠
∅, ∪z, ℘∪∪∪r))} | ||
| Definition | df-nfw 8904 | Define the class of all infima of a weak ordering relation. |
| ⊢ infw = {r,
x, y∣y = (◡r
supw x)} | ||
| Definition | df-jn 8905 | Define the class of all join operations on weak orderings. |
| ⊢ join = {r,
w∣w = {x, y, z∣((x ∈ ∪∪r ⋀ y ∈ ∪∪r) ⋀ z =
(r supw {x, y}))}} | ||
| Definition | df-mee 8906 | Define the class of all meet operations on weak orderings. |
| ⊢ meet = {r,
w∣w = {x, y, z∣((x ∈ ∪∪r ⋀ y ∈ ∪∪r) ⋀ z =
(r infw {x, y}))}} | ||
| Definition | df-la 8907 | Define the class of all lattices, which are posets in which every two elements have upper and lower bounds. |
| ⊢ Lat = {r ∈ Poset∣∀x ∈ dom r∀y ∈ dom r((r supw {x, y}) ∈ dom r ⋀ (r infw {x, y}) ∈ dom r)} | ||
| Theorem | isps 8908 | The predicate "is a poset" i.e. a transitive, reflexive, antisymmetric relation. |
| ⊢ (R ∈ A → (R ∈ Poset ↔ (Rel R ⋀ (R ∘ R) ⊆ R ⋀ (R ∩ ◡R) = (I ↾ ∪∪R)))) | ||
| Theorem | psrel 8909 | A poset is a relation. |
| ⊢ (A ∈ Poset → Rel A) | ||
| Theorem | pslem 8910 | Lemma for psref 8912 and others. |
| Theorem | psdmrn 8911 | The domain and range of a poset equal its field. |
| ⊢ (R ∈ Poset → (dom R = ∪∪R ⋀ ran R = ∪∪R)) | ||
| Theorem | psref 8912 | A poset is reflexive. |
| ⊢ X = dom R ⇒ ⊢ ((R ∈ Poset ⋀ A ∈ X) → ARA) | ||
| Theorem | psrn 8913 | The range of a poset equals it domain. |
| ⊢ X = dom R ⇒ ⊢ (R ∈ Poset → X = ran R) | ||
| Theorem | psasym 8914 | A poset is antisymmetric. |
| ⊢ ((R ∈ Poset ⋀ ARB ⋀ BRA) → A = B) | ||
| Theorem | pstr 8915 | A poset is transitive. |
| ⊢ ((R ∈ Poset ⋀ ARB ⋀ BRC) → ARC) | ||
| Theorem | spwval2 8916 | Value of supremum under a weak ordering. Read R supw A as "the R -supremum of A." ∪∪R is the field of a relation R by relfld 3621. Unlike df-sup 4718 for strong orderings, the supremum exists iff R supw A belongs to the field. |
| ⊢ X = ∪∪R & ⊢ Z = {x ∈ X∣(∀y ∈ A yRx ⋀ ∀y ∈ X (∀z ∈ A zRy → xRy))} ⇒ ⊢ ((R ∈ U ⋀ A ∈ W) → (R supw A) = if(Z ≠ ∅, ∪Z, ℘∪X)) | ||
| Theorem | spwval3 8917 | Value of a supremum. |
| ⊢ X = ∪∪R & ⊢ (φ ↔ (∀y ∈ A yRx ⋀ ∀y ∈ X (∀z ∈ A zRy → xRy))) ⇒ ⊢ ((R ∈ U ⋀ A ∈ W ⋀ ∃x ∈ X φ) → (R supw A) = ∪{x ∈ X∣φ}) | ||
| Theorem | spwnex3 8918 | When the supremum of set A doesn't exist, R supw A isn't in the the field of order relation R. |
| ⊢ X = ∪∪R & ⊢ (φ ↔ (∀y ∈ A yRx ⋀ ∀y ∈ X (∀z ∈ A zRy → xRy))) ⇒ ⊢ ((R ∈ U ⋀ A ∈ W ⋀ ¬ ∃x ∈ X φ) → ¬ (R supw A) ∈ X) | ||
| Theorem | spwmo 8919 | A poset has at most one supremum. |
| ⊢ (φ ↔ (∀y ∈ A yRx ⋀ ∀y ∈ X (∀z ∈ A zRy → xRy))) ⇒ ⊢ (R ∈ Poset → ∃*x(x ∈ X ⋀ φ)) | ||
| Theorem | spweu 8920 | A supremum is unique. |
| ⊢ (φ ↔ (∀y ∈ A yRx ⋀ ∀y ∈ X (∀z ∈ A zRy → xRy))) ⇒ ⊢ ((R ∈ Poset ⋀ ∃x ∈ X φ) → ∃!x ∈ X φ) | ||
| Theorem | spwpr2 8921 | Property of supremum defining condition for an unordered pair. |
| ⊢ (φ ↔ (∀y ∈ A yRx ⋀ ∀y ∈ X (∀z ∈ A zRy → xRy))) ⇒ ⊢ (((R ∈ T ⋀ A = {B, C}) ⋀ (B ∈ U ⋀ C ∈ W)) → (φ ↔ ((BRx ⋀ CRx) ⋀ ∀y ∈ X ((BRy ⋀ CRy) → xRy)))) | ||
| Theorem | spwval 8922 | Value of a supremum. |
| ⊢ X = dom R & ⊢ (φ ↔ (∀y ∈ A yRx ⋀ ∀y ∈ X (∀z ∈ A zRy → xRy))) ⇒ ⊢ ((R ∈ Poset ⋀ A ∈ W ⋀ ∃x ∈ X φ) → (R supw A) = ∪{x ∈ X∣φ}) | ||
| Theorem | spwcl 8923 | Closure of a supremum. |
| ⊢ X = dom R & ⊢ (φ ↔ (∀y ∈ A yRx ⋀ ∀y ∈ X (∀z ∈ A zRy → xRy))) ⇒ ⊢ ((R ∈ Poset ⋀ A ∈ W ⋀ ∃x ∈ X φ) → (R supw A) ∈ X) | ||
| Theorem | spwnex 8924 | Non-closure when the supremum doesn't exist. |
| ⊢ X = dom R & ⊢ (φ ↔ (∀y ∈ A yRx ⋀ ∀y ∈ X (∀z ∈ A zRy → xRy))) ⇒ ⊢ ((R ∈ Poset ⋀ A ∈ W ⋀ ¬ ∃x ∈ X φ) → ¬ (R supw A) ∈ X) | ||
| Theorem | spwex 8925 | A supremum exists iff R supw A belongs to the domain of R. |
| ⊢ X = dom R & ⊢ (φ ↔ (∀y ∈ A yRx ⋀ ∀y ∈ X (∀z ∈ A zRy → xRy))) ⇒ ⊢ ((R ∈ Poset ⋀ A ∈ W) → (∃x ∈ X φ ↔ (R supw A) ∈ X)) | ||
| Theorem | spwpr4 8926 | Supremum of an unordered pair. |
| ⊢ X = dom R ⇒ ⊢ (((R ∈ Poset ⋀ C ∈ D) ⋀ (ARC ⋀ BRC) ⋀ ∀x ∈ X ((ARx ⋀ BRx) → CRx)) → (R supw {A, B}) = C) | ||
| Theorem | spwpr4OLD 8927 | Supremum of an unordered pair. |
| ⊢ X = dom R ⇒ ⊢ (((R ∈ Poset ⋀ C ∈ X) ⋀ (ARC ⋀ BRC) ⋀ ∀x ∈ X ((ARx ⋀ BRx) → CRx)) → (R supw {A, B}) = C) | ||
| Theorem | spwpr4aOLD 8928 | Supremum of an unordered pair. |
| ⊢ X = dom R & ⊢ (φ ↔ (∀y ∈ {A, B}yRx ⋀ ∀y ∈ X (∀z ∈ {A, B}zRy → xRy))) ⇒ ⊢ (((R ∈ Poset ⋀ C ∈ X) ⋀ (ARC ⋀ BRC) ⋀ ∀y ∈ X ((ARy ⋀ BRy) → CRy)) → (R supw {A, B}) = C) | ||
| Theorem | spwpr4c 8929 | Supremum of an unordered pair of comparable elements. |
| ⊢ ((R ∈ Poset ⋀ B ∈ U ⋀ ARB) → (R supw {A, B}) = B) | ||
| Theorem | isla 8930 | The predicate "is a lattice" i.e. a poset in which any two elements have upper and lower bounds. |
| ⊢ X = dom R ⇒ ⊢ (R ∈ Lat ↔ (R ∈ Poset ⋀ ∀x ∈ X ∀y ∈ X ((R supw {x, y}) ∈ X ⋀ (R infw {x, y}) ∈ X))) | ||
| Theorem | laspwcl 8931 | Closure of the supremum (join) of two lattice elements. |
| ⊢ X = dom R ⇒ ⊢ ((R ∈ Lat ⋀ A ∈ X ⋀ B ∈ X) → (R supw {A, B}) ∈ X) | ||
| Theorem | lanfwcl 8932 | Closure of the infimum (meet) of two lattice elements. |
| ⊢ X = dom R ⇒ ⊢ ((R ∈ Lat ⋀ A ∈ X ⋀ B ∈ X) → (R infw {A, B}) ∈ X) | ||
| Real and complex numbers (cont.) | ||
| The exponential, sine, and cosine functions (cont.) | ||
| Theorem | sincolem 8933 | Lemma for sinco 8935 and cosco 8936. |
| Theorem | sincnlem 8934 | Lemma for sincn 8937 and coscn 8938. |
| Theorem | sinco 8935 | Sine expressed as a function composition. (Contributed by Paul Chapman, 28-Nov-2007.) |
| ⊢ F = {x, y∣(x ∈ ℂ ⋀ y =
(i · x))}
& ⊢
G = {x,
y∣(x ∈ ℂ ⋀ y = (-i · x))} & ⊢ J = {x, y∣(x ∈ ℂ ⋀ y = (x / (2
· i)))} & ⊢ H = {w, v∣(w ∈ ℂ ⋀ v = (((exp ∘
F) ‘w) − ((exp ∘ G)
‘w)))} ⇒ ⊢ sin = (J
∘ H) | ||
| Theorem | cosco 8936 | Cosine expressed as a function composition. (Contributed by Paul Chapman, 28-Nov-2007.) |
| ⊢ F = {x, y∣(x ∈ ℂ ⋀ y =
(i · x))}
& ⊢
G = {x,
y∣(x ∈ ℂ ⋀ y = (-i · x))} & ⊢ J = {x, y∣(x ∈ ℂ ⋀ y = (x /
2))} & ⊢ H = {w, v∣(w ∈ ℂ ⋀ v = (((exp
∘ F)
‘w) + ((exp ∘ G)
‘w)))} ⇒ ⊢ cos = (J
∘ H) | ||
| Theorem | sincn 8937 | Sine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) |
| ⊢ sin ∈ (ℂ–cn→ℂ) | ||
| Theorem | coscn 8938 | Cosine is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) |
| ⊢ cos ∈ (ℂ–cn→ℂ) | ||
| Properties of pi = 3.14159... | ||
| Theorem | pilem1 8939 | Lemma for pire 8945, pigt2lt4 8943 and sinpi 8944. |
| Theorem | pilem2 8940 | Lemma for pire 8945, pigt2lt4 8943 and sinpi 8944. |
| Theorem | pilem3 8941 | Lemma for pire 8945, pigt2lt4 8943 and sinpi 8944. |
| Theorem | pilem4 8942 | Lemma for pire 8945, pigt2lt4 8943 and sinpi 8944. |
| Theorem | pigt2lt4 8943 | π is between 2 and 4. (Contributed by Paul Chapman, 23-Jan-2008.) |
| ⊢ (2 < π ⋀ π < 4) | ||
| Theorem | sinpi 8944 | The sine of π is 0. (Contributed by Paul Chapman, 23-Jan-2008.) |
| ⊢ (sin ‘π) = 0 | ||
| Theorem | pire 8945 | π is a real number. (Contributed by Paul Chapman, 23-Jan-2008.) |
| ⊢ π ∈ ℝ | ||
| Theorem | pipos 8946 | π is positive. (Contributed by Paul Chapman, 23-Jan-2008.) |
| ⊢ 0 < π | ||
| Theorem | sinhalfpilem 8947 | Lemma for sinhalfpi 8948 and coshalfpi 8949. |
| Theorem | sinhalfpi 8948 | The sine of π / 2 is 1. (Contributed by Paul Chapman, 23-Jan-2008.) |
| ⊢ (sin ‘(π / 2)) = 1 | ||
| Theorem | coshalfpi 8949 | The cosine of π / 2 is 0. (Contributed by Paul Chapman, 23-Jan-2008.) |
| ⊢ (cos ‘(π / 2)) = 0 | ||
| Theorem | cospi 8950 | The cosine of π is -1. (Contributed by Paul Chapman, 23-Jan-2008.) |
| ⊢ (cos ‘π) = -1 | ||
| Theorem | eulerid 8951 | Euler's identity. (Contributed by Paul Chapman, 23-Jan-2008.) |
| ⊢ ((exp ‘(i · π)) + 1) = 0 | ||
| Theorem | sin2pi 8952 | The sine of 2π is 0. (Contributed by Paul Chapman, 23-Jan-2008.) |
| ⊢ (sin ‘(2 · π)) = 0 | ||
| Theorem | cos2pi 8953 | The cosine of 2π is 1. (Contributed by Paul Chapman, 23-Jan-2008.) |
| ⊢ (cos ‘(2 · π)) = 1 | ||
| Theorem | sinperlem1 8954 | Lemma for sin2kpi 8956 and cos2kpi 8957. |
| Theorem | sinperlem2 8955 | Lemma for sin2kpi 8956 and cos2kpi 8957. |
| Theorem | sin2kpi 8956 | If K is an integer, the sine of 2Kπ is 0. (Contributed by Paul Chapman, 23-Jan-2008.) |
| ⊢ (K ∈ ℤ → (sin ‘(K · (2 · π))) = 0) | ||
| Theorem | cos2kpi 8957 | If K is an integer, the cosine of 2Kπ is 1. (Contributed by Paul Chapman, 23-Jan-2008.) |
| ⊢ (K ∈ ℤ → (cos ‘(K · (2 · π))) = 1) | ||
| Theorem | sinper 8958 | The sine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) |
| ⊢ ((A ∈ ℂ ⋀ K ∈ ℤ) → (sin ‘(A + (K · (2 · π)))) = (sin ‘A)) | ||
| Theorem | cosper 8959 | The cosine function is periodic. (Contributed by Paul Chapman, 23-Jan-2008.) |
| ⊢ ((A ∈ ℂ ⋀ K ∈ ℤ) → (cos ‘(A + (K · (2 · π)))) = (cos ‘A)) | ||
| Theorem | sin2pim 8960 | Sine of a number subtracted from 2 · π. (Contributed by Paul Chapman, 15-Mar-2008.) |
| ⊢ (A ∈ ℂ → (sin ‘((2 · π) − A)) = -(sin ‘A)) | ||
| Theorem | cos2pim 8961 | Cosine of a number subtracted from 2 · π. (Contributed by Paul Chapman, 15-Mar-2008.) |
| ⊢ (A ∈ ℂ → (cos ‘((2 · π) − A)) = (cos ‘A)) | ||
| Theorem | sinmpi 8962 | Sine of a number less π. (Contributed by Paul Chapman, 15-Mar-2008.) |
| ⊢ (A ∈ ℂ → (sin ‘(A − π)) = -(sin ‘A)) | ||
| Theorem | cosmpi 8963 | Cosine of a number less π. (Contributed by Paul Chapman, 15-Mar-2008.) |
| ⊢ (A ∈ ℂ → (cos ‘(A − π)) = -(cos ‘A)) | ||
| Theorem | sinppi 8964 | Sine of a number plus π. |
| ⊢ (A ∈ ℂ → (sin ‘(A + π)) = -(sin ‘A)) | ||
| Theorem | cosppi 8965 | Cosine of a complex number plus π. |
| ⊢ (A ∈ ℂ → (cos ‘(A + π)) = -(cos ‘A)) | ||
| Theorem | efimpi 8966 | The exponential function of i times a real number less π. (Contributed by Paul Chapman, 15-Mar-2008.) |
| ⊢ (A ∈ ℂ → (exp ‘(i · (A − π))) = -(exp ‘(i · A))) | ||
| Theorem | sinhalfpip 8967 | The sine of π / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.) |
| ⊢ (A ∈ ℂ → (sin ‘((π / 2) + A)) = (cos ‘A)) | ||
| Theorem | sinhalfpim 8968 | The sine of π / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.) |
| ⊢ (A ∈ ℂ → (sin ‘((π / 2) − A)) = (cos ‘A)) | ||
| Theorem | coshalfpip 8969 | The cosine of π / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008.) |
| ⊢ (A ∈ ℂ → (cos ‘((π / 2) + A)) = -(sin ‘A)) | ||
| Theorem | coshalfpim 8970 | The cosine of π / 2 minus a number. (Contributed by Paul Chapman, 24-Jan-2008.) |
| ⊢ (A ∈ ℂ → (cos ‘((π / 2) − A)) = (sin ‘A)) | ||
| Theorem | sincosq1lem 8971 | Lemma for sincosq1sgn 8972. |
| Theorem | sincosq1sgn 8972 | The signs of the sine and cosine functions in the first quadrant. (Contributed by Paul Chapman, 24-Jan-2008.) |
| ⊢ (A ∈ (0(,)(π / 2)) → (0 < (sin ‘A) ⋀ 0 < (cos ‘A))) | ||
| Theorem | sincosq2sgn 8973 | The signs of the sine and cosine functions in the second quadrant. (Contributed by Paul Chapman, 24-Jan-2008.) |
| ⊢ (A ∈ ((π / 2)(,)π) → (0 < (sin ‘A) ⋀ (cos ‘A) < 0)) | ||
| Theorem | sincosq3sgn 8974 | The signs of the sine and cosine functions in the third quadrant. (Contributed by Paul Chapman, 24-Jan-2008.) |
| ⊢ (A ∈ (π(,)(3 · (π / 2))) → ((sin ‘A) < 0 ⋀ (cos ‘A) < 0)) | ||
| Theorem | sincosq4sgn 8975 | The signs of the sine and cosine functions in the fourth quadrant. (Contributed by Paul Chapman, 24-Jan-2008.) |
| ⊢ (A ∈ ((3 · (π / 2))(,)(2 · π)) → ((sin ‘A) < 0 ⋀ 0 < (cos ‘A))) | ||
| Theorem | sinq12gt0t 8976 | The sine of a number strictly between 0 and π is positive. (Contributed by Paul Chapman, 15-Mar-2008.) |
| ⊢ (A ∈ (0(,)π) → 0 < (sin ‘A)) | ||
| Theorem | sinq34lt0t 8977 | The sine of a number strictly between π and 2 · π is negative. |
| ⊢ (A ∈ (π(,)(2 · π)) → (sin ‘A) < 0) | ||
| Theorem | sincosq1eq 8978 | Complementarity of the sine and cosine functions in the first quadrant. (Contributed by Paul Chapman, 25-Jan-2008.) |
| ⊢ ((A ∈ ℂ ⋀ B ∈ ℂ ⋀ (A + B) = 1) → (sin ‘(A · (π / 2))) = (cos ‘(B · (π / 2)))) | ||
| Theorem | sincos4thpi 8979 | The sine and cosine of π / 4. (Contributed by Paul Chapman, 25-Jan-2008.) |
| ⊢ ((sin ‘(π / 4)) = (1 / (√ ‘2)) ⋀ (cos ‘(π / 4)) = (1 / (√ ‘2))) | ||
| Theorem | sincos6thpi 8980 | The sine and cosine of π / 6. (Contributed by Paul Chapman, 25-Jan-2008.) |
| ⊢ ((sin ‘(π / 6)) = (1 / 2) ⋀ (cos ‘(π / 6)) = ((√ ‘3) / 2)) | ||
| Theorem | abssinper 8981 | The absolute value of sine has period π. |
| ⊢ ((A ∈ ℂ ⋀ K ∈ ℤ) → (abs ‘(sin ‘(A + (K · π)))) = (abs ‘(sin ‘A))) | ||
| Theorem | sinkpi 8982 | The sine of an integer multiple of π is 0. |
| ⊢ (K ∈ ℤ → (sin ‘(K · π)) = 0) | ||
| Theorem | coskpi 8983 | The absolute value of the cosine of an integer multiple of π is 1. |
| ⊢ (K ∈ ℤ → (abs ‘(cos ‘(K · π))) = 1) | ||
| Theorem | sineq0 8984 | A real number whose sine is zero is an integer multiple of π. |
| ⊢ ((A ∈ ℝ ⋀ (sin ‘A) = 0) → A = ((⌊ ‘(A / π)) · π)) | ||
| Theorem | sineq0OLD 8985 | A real number whose sine is zero is an integer multiple of π. |
| ⊢ ((A ∈ ℝ ⋀ (sin ‘A) = 0) → A = ((⌊ ‘(A / π)) · π)) | ||
| Theorem | sineq0re 8986 | A number whose sine is zero is real. This theorem can be used to extend sineq0 8984 to complex numbers. |
| ⊢ ((A ∈ ℂ ⋀ (sin ‘A) = 0) → A ∈ ℝ) | ||
| Theorem | cosh111lem1 8987 | Lemma for cosh111 8990. |
| Theorem | cosh111lem2 8988 | Lemma for cosh111 8990. |
| Theorem | cosh111lem3 8989 | Lemma for cosh111 8990. |
| Theorem | cosh111 8990 | Cosine is one-to-one over the closed-below, open-above interval from 0 to π. (Contributed by Paul Chapman, 16-Mar-2008.) |
| ⊢ ((A ∈ (0[,)π) ⋀ B ∈ (0[,)π)) → (A = B ↔ (cos ‘A) = (cos ‘B))) | ||
| Mapping of the exponential function | ||
| Theorem | efgh 8991 | The exponential function of a scaled complex number is a group homomorphism from the group of complex numbers under addition to the set of complex numbers under multiplication. (Contributed by Paul Chapman, 25-Apr-2008.) |
| ⊢ F = {x, y∣(x ∈ ℂ ⋀ y = (exp
‘(A · x)))} ⇒ ⊢ ((A ∈ ℂ ⋀ B ∈ ℂ ⋀ C ∈ ℂ) →
(F ‘(B + C)) =
((F ‘B) · (F
‘C))) | ||
| Theorem | efghgrpilem 8992 | Lemma for efghgrpi 8993, |
| Theorem | efghgrpi 8993 | The image of a subgroup of the group +, under the exponential function of a scaled complex number, is an Abelian group. (Contributed by Paul Chapman, 25-Apr-2008.) |
| ⊢ S = {y∣∃x ∈ X y = (exp ‘(A · x))} & ⊢ G = ( · ↾ (S × S)) & ⊢ A ∈ ℂ & ⊢ X ⊆ ℂ & ⊢ ( + ↾ (X × X)) ∈ (SubGrp ‘ + ) ⇒ ⊢ G ∈ Abel | ||
| Theorem | efif 8994 | The exponential function of an imaginary number maps the closed-below, open-above interval from 0 to 2 · π to the unit circle. (Contributed by Paul Chapman, 16-Mar-2008.) |
| ⊢ F = {x, y∣(x ∈ (0[,)(2 · π)) ⋀ y = (exp
‘(i · x)))}
& ⊢
S = {z ∈ ℂ∣(abs
‘z) = 1} ⇒ ⊢ F:(0[,)(2
· π))–→S | ||
| Theorem | efifolem1 8995 | Lemma for efifo 9002. |
| Theorem | efifolem2 8996 | Lemma for efifo 9002. |
| Theorem | efifolem3 8997 | Lemma for efifo 9002. |
| Theorem | efifolem4 8998 | Lemma for efifo 9002. |
| Theorem | efifolem5 8999 | Lemma for efifo 9002. |
| Theorem | efifolem6 9000 | Lemma for efifo 9002. |
| MPE Home Contents | Copyright terms: Public domain | < Previous Next > |