/
fa.thy
48 lines (36 loc) · 959 Bytes
/
fa.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
Require Sets.
Require Number.
Require Algebra.
Require Metric.
(** Real vector space *)
Definition VectorSpace
(I : Number.Integer)
(R : Number.Real I) :=
Algebra.LeftModule R.
(** Normed space *)
Definition Norm
(I : Number.Integer)
(R : Number.Real I)
(V : VectorSpace I R) :=
thy
Parameter norm : V.s -> R.real.
Axiom norm_nonnegative:
forall x : V.s, R.leq R.zero (norm x).
Axiom norm_zero:
forall x : V.s, norm x = R.zero -> x = V.zero.
Axiom norm_homogeneous:
forall x : V.s, forall a : R.real, norm (V.act a x) = R.mul (R.abs a) (norm x).
Axiom norm_triangle:
forall x y : V.s, R.leq (norm (V.add x y)) (R.add (norm x) (norm y)).
end.
(** Banach space. *)
Definition BanachSpace :=
fun (I : Number.Integer) =>
fun (R : Number.Real I) =>
fun (V : VectorSpace I R) =>
thy
include Norm I R V.
include Metric.CompleteMetric I R V.
Axiom dist_from_norm:
forall x y : V.s, dist x y = norm (V.sub x y).
end.