-(*
-lemma eq_opp_x_times_opp_one_x: ∀F:ordered_field_ch0.∀x:F.-x = -1*x.
- intros;
-
-lemma not_eq_x_zero_to_lt_zero_mult_x_x:
- ∀F:ordered_field_ch0.∀x:F. x ≠ 0 → 0 < x * x.
- intros;
- elim (of_weak_tricotomy ? ? ? ? ? ? ? ? F ? ? H);
- [ generalize in match (le_x_zero_to_le_zero_opp_x F ? H1); intro;
- generalize in match (of_mult_compat ? ? ? ? ? ? ? ? F ? ? H2 H2); intro;
-*)
-
-axiom not_eq_sum_field_zero: ∀F,n. n > O → sum_field F n ≠ 0.
-
-record is_vector_space (K: field) (G:abelian_group) (emult:K→G→G) : Prop
-≝
- { vs_nilpotent: ∀v. emult 0 v = 0;
- vs_neutral: ∀v. emult 1 v = v;
- vs_distributive: ∀a,b,v. emult (a + b) v = (emult a v) + (emult b v);
- vs_associative: ∀a,b,v. emult (a * b) v = emult a (emult b v)
- }.
-
-record vector_space (K:field): Type \def
-{ vs_abelian_group :> abelian_group;
- emult: K → vs_abelian_group → vs_abelian_group;
- vs_vector_space_properties :> is_vector_space K vs_abelian_group emult
-}.
-
-interpretation "Vector space external product" 'times a b =
- (cic:/matita/integration_algebras/emult.con _ _ a b).
-
-record is_lattice (C:Type) (join,meet:C→C→C) : Prop \def
- { (* abelian semigroup properties *)
- l_comm_j: symmetric ? join;
- l_associative_j: associative ? join;
- l_comm_m: symmetric ? meet;
- l_associative_m: associative ? meet;
- (* other properties *)
- l_adsorb_j_m: ∀f,g. join f (meet f g) = f;
- l_adsorb_m_j: ∀f,g. meet f (join f g) = f
- }.
-
-record lattice (C:Type) : Type \def
- { join: C → C → C;
- meet: C → C → C;
- l_lattice_properties: is_lattice ? join meet
- }.
-
-definition le \def λC:Type.λL:lattice C.λf,g. meet ? L f g = f.
-
-interpretation "Lattice le" 'leq a b =
- (cic:/matita/integration_algebras/le.con _ _ a b).
-
-definition carrier_of_lattice ≝
- λC:Type.λL:lattice C.C.
-
-record is_riesz_space (K:ordered_field_ch0) (V:vector_space K)
- (L:lattice (Type_OF_vector_space ? V))
-: Prop
-\def
- { rs_compat_le_plus: ∀f,g,h. le ? L f g → le ? L (f+h) (g+h);
- rs_compat_le_times: ∀a:K.∀f. of_le ? 0 a → le ? L 0 f → le ? L 0 (a*f)
- }.
-
-record riesz_space : Type \def
- { rs_ordered_field_ch0: ordered_field_ch0;
- rs_vector_space:> vector_space rs_ordered_field_ch0;
- rs_lattice:> lattice rs_vector_space;
- rs_riesz_space_properties: is_riesz_space ? rs_vector_space rs_lattice
- }.
-
-definition absolute_value \def λS:riesz_space.λf.join ? S f (-f).
-
-record is_archimedean_riesz_space (S:riesz_space) : Prop
-\def
- { ars_archimedean: ∃u.∀n.∀a.∀p:n > O.
- le ? S
- (absolute_value S a)
- (emult ? S
- (inv ? (sum_field (rs_ordered_field_ch0 S) n) (not_eq_sum_field_zero ? n p))
- u) →
- a = 0
- }.
-
-record archimedean_riesz_space : Type \def
- { ars_riesz_space:> riesz_space;
- ars_archimedean_property: is_archimedean_riesz_space ars_riesz_space
- }.