- (cic:/matita/lattices/l_join.con _ a b).
-
-definition le \def λL:lattice.λf,g:L. (f ∧ g) = f.
-
-definition ordered_set_of_lattice: lattice → ordered_set.
- intros (L);
- apply mk_ordered_set;
- [2: apply (le L)
- | skip
- | apply mk_is_order_relation;
- [ unfold reflexive;
- intros;
- unfold;
- rewrite < (l_adsorb_j_m ? ? ? L ? x) in ⊢ (? ? (? ? ? %) ?);
- rewrite > l_adsorb_m_j;
- [ reflexivity
- | apply (l_lattice_properties L)
- ]
- | intros;
- unfold transitive;
- unfold le;
- intros;
- rewrite < H;
- rewrite > (l_associative_m ? ? ? L);
- rewrite > H1;
- reflexivity
- | unfold antisimmetric;
- unfold le;
- intros;
- rewrite < H;
- rewrite > (l_comm_m ? ? ? L);
- assumption
- ]
- ]
-qed.
+ (cic:/matita/lattice/meet.con (cic:/matita/lattice/latt_jcarr.con _) a b).
+
+record lattice : Type ≝ {
+ latt_carr:> lattice_;
+ absorbjm: ∀f,g:latt_carr. (f ∨ (f ∧ g)) ≈ f;
+ absorbmj: ∀f,g:latt_carr. (f ∧ (f ∨ g)) ≈ f
+}.
+
+notation "'meet'" non associative with precedence 50 for @{'meet}.
+notation "'meet_refl'" non associative with precedence 50 for @{'meet_refl}.
+notation "'meet_comm'" non associative with precedence 50 for @{'meet_comm}.
+notation "'meet_assoc'" non associative with precedence 50 for @{'meet_assoc}.
+notation "'strong_extm'" non associative with precedence 50 for @{'strong_extm}.
+notation "'le_to_eqm'" non associative with precedence 50 for @{'le_to_eqm}.
+notation "'lem'" non associative with precedence 50 for @{'lem}.
+notation "'join'" non associative with precedence 50 for @{'join}.
+notation "'join_refl'" non associative with precedence 50 for @{'join_refl}.
+notation "'join_comm'" non associative with precedence 50 for @{'join_comm}.
+notation "'join_assoc'" non associative with precedence 50 for @{'join_assoc}.
+notation "'strong_extj'" non associative with precedence 50 for @{'strong_extj}.
+notation "'le_to_eqj'" non associative with precedence 50 for @{'le_to_eqj}.
+notation "'lej'" non associative with precedence 50 for @{'lej}.
+
+interpretation "Lattice meet" 'meet = (cic:/matita/lattice/meet.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice meet_refl" 'meet_refl = (cic:/matita/lattice/meet_refl.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice meet_comm" 'meet_comm = (cic:/matita/lattice/meet_comm.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice meet_assoc" 'meet_assoc = (cic:/matita/lattice/meet_assoc.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice strong_extm" 'strong_extm = (cic:/matita/lattice/strong_extm.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice le_to_eqm" 'le_to_eqm = (cic:/matita/lattice/le_to_eqm.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice lem" 'lem = (cic:/matita/lattice/lem.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice join" 'join = (cic:/matita/lattice/meet.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice join_refl" 'join_refl = (cic:/matita/lattice/meet_refl.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice join_comm" 'join_comm = (cic:/matita/lattice/meet_comm.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice join_assoc" 'join_assoc = (cic:/matita/lattice/meet_assoc.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice strong_extm" 'strong_extj = (cic:/matita/lattice/strong_extm.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice le_to_eqj" 'le_to_eqj = (cic:/matita/lattice/le_to_eqm.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice lej" 'lej = (cic:/matita/lattice/lem.con (cic:/matita/lattice/latt_jcarr.con _)).
+
+notation "'feq_jl'" non associative with precedence 50 for @{'feq_jl}.
+notation "'feq_jr'" non associative with precedence 50 for @{'feq_jr}.
+interpretation "Lattice feq_jl" 'feq_jl = (cic:/matita/lattice/feq_ml.con (cic:/matita/lattice/latt_jcarr.con _)).
+interpretation "Lattice feq_jr" 'feq_jr = (cic:/matita/lattice/feq_mr.con (cic:/matita/lattice/latt_jcarr.con _)).
+notation "'feq_ml'" non associative with precedence 50 for @{'feq_ml}.
+notation "'feq_mr'" non associative with precedence 50 for @{'feq_mr}.
+interpretation "Lattice feq_ml" 'feq_ml = (cic:/matita/lattice/feq_ml.con (cic:/matita/lattice/latt_mcarr.con _)).
+interpretation "Lattice feq_mr" 'feq_mr = (cic:/matita/lattice/feq_mr.con (cic:/matita/lattice/latt_mcarr.con _)).