author | wenzelm |
Sun, 04 Jun 2000 19:39:29 +0200 | |
changeset 9035 | 371f023d3dbd |
parent 8659 | 5fdbe2dd54f9 |
child 9374 | 153853af318b |
permissions | -rw-r--r-- |
7566 | 1 |
(* Title: HOL/Real/HahnBanach/Bounds.thy |
2 |
ID: $Id$ |
|
3 |
Author: Gertrud Bauer, TU Munich |
|
4 |
*) |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
5 |
|
9035 | 6 |
header {* Bounds *} |
7808 | 7 |
|
9035 | 8 |
theory Bounds = Main + Real: |
8659 | 9 |
(*<*) |
9035 | 10 |
subsection {* The sets of lower and upper bounds *} |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
11 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
12 |
constdefs |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
13 |
is_LowerBound :: "('a::order) set => 'a set => 'a => bool" |
7917 | 14 |
"is_LowerBound A B == \<lambda>x. x:A & (ALL y:B. x <= y)" |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
15 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
16 |
LowerBounds :: "('a::order) set => 'a set => 'a set" |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
17 |
"LowerBounds A B == Collect (is_LowerBound A B)" |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
18 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
19 |
is_UpperBound :: "('a::order) set => 'a set => 'a => bool" |
7917 | 20 |
"is_UpperBound A B == \<lambda>x. x:A & (ALL y:B. y <= x)" |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
21 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
22 |
UpperBounds :: "('a::order) set => 'a set => 'a set" |
9035 | 23 |
"UpperBounds A B == Collect (is_UpperBound A B)" |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
24 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
25 |
syntax |
7808 | 26 |
"_UPPERS" :: "[pttrn, 'a set, 'a => bool] => 'a set" |
27 |
("(3UPPER'_BOUNDS _:_./ _)" 10) |
|
28 |
"_UPPERS_U" :: "[pttrn, 'a => bool] => 'a set" |
|
29 |
("(3UPPER'_BOUNDS _./ _)" 10) |
|
30 |
"_LOWERS" :: "[pttrn, 'a set, 'a => bool] => 'a set" |
|
31 |
("(3LOWER'_BOUNDS _:_./ _)" 10) |
|
32 |
"_LOWERS_U" :: "[pttrn, 'a => bool] => 'a set" |
|
9035 | 33 |
("(3LOWER'_BOUNDS _./ _)" 10) |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
34 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
35 |
translations |
7917 | 36 |
"UPPER_BOUNDS x:A. P" == "UpperBounds A (Collect (\<lambda>x. P))" |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
37 |
"UPPER_BOUNDS x. P" == "UPPER_BOUNDS x:UNIV. P" |
7917 | 38 |
"LOWER_BOUNDS x:A. P" == "LowerBounds A (Collect (\<lambda>x. P))" |
9035 | 39 |
"LOWER_BOUNDS x. P" == "LOWER_BOUNDS x:UNIV. P" |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
40 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
41 |
|
9035 | 42 |
subsection {* Least and greatest elements *} |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
43 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
44 |
constdefs |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
45 |
is_Least :: "('a::order) set => 'a => bool" |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
46 |
"is_Least B == is_LowerBound B B" |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
47 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
48 |
Least :: "('a::order) set => 'a" |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
49 |
"Least B == Eps (is_Least B)" |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
50 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
51 |
is_Greatest :: "('a::order) set => 'a => bool" |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
52 |
"is_Greatest B == is_UpperBound B B" |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
53 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
54 |
Greatest :: "('a::order) set => 'a" |
9035 | 55 |
"Greatest B == Eps (is_Greatest B)" |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
56 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
57 |
syntax |
7808 | 58 |
"_LEAST" :: "[pttrn, 'a => bool] => 'a" |
59 |
("(3LLEAST _./ _)" 10) |
|
60 |
"_GREATEST" :: "[pttrn, 'a => bool] => 'a" |
|
9035 | 61 |
("(3GREATEST _./ _)" 10) |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
62 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
63 |
translations |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
64 |
"LLEAST x. P" == "Least {x. P}" |
9035 | 65 |
"GREATEST x. P" == "Greatest {x. P}" |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
66 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
67 |
|
9035 | 68 |
subsection {* Infimum and Supremum *} |
8585 | 69 |
(*>*) |
7978 | 70 |
text {* |
71 |
A supremum\footnote{The definition of the supremum is based on one in |
|
72 |
\url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Lubs.html}} of |
|
73 |
an ordered set $B$ w.~r.~t.~$A$ is defined as a least upper bound of |
|
74 |
$B$, which lies in $A$. |
|
9035 | 75 |
*} |
7917 | 76 |
|
77 |
text{* If a supremum exists, then $\idt{Sup}\ap A\ap B$ |
|
9035 | 78 |
is equal to the supremum. *} |
7917 | 79 |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
80 |
constdefs |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
81 |
is_Sup :: "('a::order) set => 'a set => 'a => bool" |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
82 |
"is_Sup A B x == isLub A B x" |
7917 | 83 |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
84 |
Sup :: "('a::order) set => 'a set => 'a" |
9035 | 85 |
"Sup A B == Eps (is_Sup A B)" |
8659 | 86 |
(*<*) |
7917 | 87 |
constdefs |
88 |
is_Inf :: "('a::order) set => 'a set => 'a => bool" |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
89 |
"is_Inf A B x == x:A & is_Greatest (LowerBounds A B) x" |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
90 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
91 |
Inf :: "('a::order) set => 'a set => 'a" |
9035 | 92 |
"Inf A B == Eps (is_Inf A B)" |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
93 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
94 |
syntax |
7917 | 95 |
"_SUP" :: "[pttrn, 'a set, 'a => bool] => 'a set" |
7808 | 96 |
("(3SUP _:_./ _)" 10) |
7917 | 97 |
"_SUP_U" :: "[pttrn, 'a => bool] => 'a set" |
7808 | 98 |
("(3SUP _./ _)" 10) |
7917 | 99 |
"_INF" :: "[pttrn, 'a set, 'a => bool] => 'a set" |
7808 | 100 |
("(3INF _:_./ _)" 10) |
7917 | 101 |
"_INF_U" :: "[pttrn, 'a => bool] => 'a set" |
9035 | 102 |
("(3INF _./ _)" 10) |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
103 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
104 |
translations |
7917 | 105 |
"SUP x:A. P" == "Sup A (Collect (\<lambda>x. P))" |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
106 |
"SUP x. P" == "SUP x:UNIV. P" |
7917 | 107 |
"INF x:A. P" == "Inf A (Collect (\<lambda>x. P))" |
9035 | 108 |
"INF x. P" == "INF x:UNIV. P" |
8585 | 109 |
(*>*) |
7978 | 110 |
text{* The supremum of $B$ is less than any upper bound |
9035 | 111 |
of $B$.*} |
7917 | 112 |
|
9035 | 113 |
lemma sup_le_ub: "isUb A B y ==> is_Sup A B s ==> s <= y" |
114 |
by (unfold is_Sup_def, rule isLub_le_isUb) |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
115 |
|
9035 | 116 |
text {* The supremum $B$ is an upper bound for $B$. *} |
7917 | 117 |
|
9035 | 118 |
lemma sup_ub: "y:B ==> is_Sup A B s ==> y <= s" |
119 |
by (unfold is_Sup_def, rule isLubD2) |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
120 |
|
7917 | 121 |
text{* The supremum of a non-empty set $B$ is greater |
9035 | 122 |
than a lower bound of $B$. *} |
7917 | 123 |
|
124 |
lemma sup_ub1: |
|
9035 | 125 |
"[| ALL y:B. a <= y; is_Sup A B s; x:B |] ==> a <= s" |
126 |
proof - |
|
127 |
assume "ALL y:B. a <= y" "is_Sup A B s" "x:B" |
|
128 |
have "a <= x" by (rule bspec) |
|
129 |
also have "x <= s" by (rule sup_ub) |
|
130 |
finally show "a <= s" . |
|
131 |
qed |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
132 |
|
9035 | 133 |
end |