-record is_riesz_space (K:ordered_field_ch0) (V:vector_space K)
- (L:lattice V)
-: Prop
-\def
- { rs_compat_le_plus: ∀f,g,h:V. os_le ? L f g → os_le ? L (f+h) (g+h);
- rs_compat_le_times: ∀a:K.∀f:V. zero K≤a → os_le ? L (zero V) f → os_le ? L (zero V) (a*f)
+record pre_riesz_space (K:ordered_field_ch0) : Type \def
+ { rs_vector_space:> vector_space K;
+ rs_lattice_: lattice;
+ rs_with: os_carrier rs_lattice_ = rs_vector_space
+ }.
+
+lemma rs_lattice: ∀K:ordered_field_ch0.pre_riesz_space K → lattice.
+ intros (K V);
+ apply mk_lattice;
+ [ apply (carrier V)
+ | apply (eq_rect ? ? (λC:Type.C→C→C) ? ? (rs_with ? V));
+ apply l_join
+ | apply (eq_rect ? ? (λC:Type.C→C→C) ? ? (rs_with ? V));
+ apply l_meet
+ | apply
+ (eq_rect' ? ?
+ (λa:Type.λH:os_carrier (rs_lattice_ ? V)=a.
+ is_lattice a
+ (eq_rect Type (rs_lattice_ K V) (λC:Type.C→C→C)
+ (l_join (rs_lattice_ K V)) a H)
+ (eq_rect Type (rs_lattice_ K V) (λC:Type.C→C→C)
+ (l_meet (rs_lattice_ K V)) a H))
+ ? ? (rs_with ? V));
+ simplify;
+ apply l_lattice_properties
+ ].
+qed.
+
+coercion cic:/matita/integration_algebras/rs_lattice.con.
+
+record is_riesz_space (K:ordered_field_ch0) (V:pre_riesz_space K) : Prop ≝
+ { rs_compat_le_plus: ∀f,g,h:V. f≤g → f+h≤g+h;
+ rs_compat_le_times: ∀a:K.∀f:V. zero K≤a → zero V≤f → zero V≤a*f