- 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.