bs_cotransitive: cotransitive ? bs_apart
}.
-notation "hvbox(a break # b)" non associative with precedence 50
+notation "hvbox(a break # b)" non associative with precedence 45
for @{ 'apart $a $b}.
-interpretation "bishop_setapartness" 'apart x y =
- (cic:/matita/dama/bishop_set/bs_apart.con _ x y).
+interpretation "bishop_setapartness" 'apart x y = (bs_apart _ x y).
definition bishop_set_of_ordered_set: ordered_set → bishop_set.
intros (E); apply (mk_bishop_set E (λa,b:E. a ≰ b ∨ b ≰ a));
(* Definition 2.2 (2) *)
definition eq ≝ λA:bishop_set.λa,b:A. ¬ (a # b).
-notation "hvbox(a break ≈ b)" non associative with precedence 50
+notation "hvbox(a break ≈ b)" non associative with precedence 45
for @{ 'napart $a $b}.
-interpretation "Bishop set alikeness" 'napart a b =
- (cic:/matita/dama/bishop_set/eq.con _ a b).
+interpretation "Bishop set alikeness" 'napart a b = (eq _ a b).
lemma eq_reflexive:∀E:bishop_set. reflexive ? (eq E).
intros (E); unfold; intros (x); apply bs_coreflexive;
definition lt ≝ λE:ordered_set.λa,b:E. a ≤ b ∧ a # b.
-interpretation "ordered sets less than" 'lt a b =
- (cic:/matita/dama/bishop_set/lt.con _ a b).
+interpretation "ordered sets less than" 'lt a b = (lt _ a b).
lemma lt_coreflexive: ∀E.coreflexive ? (lt E).
intros 2 (E x); intro H; cases H (_ ABS);