From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 22 May 2019 13:43:08 +0200
Subject: htmldoc regenerated
---
docs/htmldoc/mathcomp.algebra.interval.html | 598 +++++++++++++++++++---------
1 file changed, 417 insertions(+), 181 deletions(-)
(limited to 'docs/htmldoc/mathcomp.algebra.interval.html')
diff --git a/docs/htmldoc/mathcomp.algebra.interval.html b/docs/htmldoc/mathcomp.algebra.interval.html
index d10a18d..e0e16ed 100644
--- a/docs/htmldoc/mathcomp.algebra.interval.html
+++ b/docs/htmldoc/mathcomp.algebra.interval.html
@@ -21,7 +21,6 @@
@@ -76,31 +75,228 @@
-Section IntervalPo.
+Section LersifPo.
-CoInductive itv_bound (T : Type) : Type := BOpen_if of bool & T | BInfty.
-Notation BOpen := (BOpen_if true).
-Notation BClose := (BOpen_if false).
-CoInductive interval (T : Type) := Interval of itv_bound T & itv_bound T.
+Variable R : numDomainType.
-Variable (R : numDomainType).
+Definition lersif (x y : R) b := if b then x < y else x ≤ y.
-Definition pred_of_itv (i : interval R) : pred R :=
- [pred x | let: Interval l u := i in
- match l with
- | BOpen a ⇒ a < x
- | BClose a ⇒ a ≤ x
- | BInfty ⇒ true
- end &&
- match u with
- | BOpen b ⇒ x < b
- | BClose b ⇒ x ≤ b
- | BInfty ⇒ true
- end].
-Canonical Structure itvPredType := Eval hnf in mkPredType pred_of_itv.
+
+
+Lemma subr_lersifr0 b (x y : R) : (y - x ≤ 0 ?< if b) = (y ≤ x ?< if b).
+
+
+Lemma subr_lersif0r b (x y : R) : (0 ≤ y - x ?< if b) = (x ≤ y ?< if b).
+
+
+Definition subr_lersif0 := (subr_lersifr0, subr_lersif0r).
+
+
+Lemma lersif_trans x y z b1 b2 :
+ x ≤ y ?< if b1 → y ≤ z ?< if b2 → x ≤ z ?< if b1 || b2.
+
+
+Lemma lersif01 b : 0 ≤ 1 ?< if b.
+
+
+Lemma lersif_anti b1 b2 x y :
+ (x ≤ y ?< if b1) && (y ≤ x ?< if b2) =
+ if b1 || b2 then false else x == y.
+
+
+Lemma lersifxx x b : (x ≤ x ?< if b) = ~~ b.
+
+
+Lemma lersifNF x y b : y ≤ x ?< if ~~ b → x ≤ y ?< if b = false.
+
+
+Lemma lersifS x y b : x < y → x ≤ y ?< if b.
+
+
+Lemma lersifT x y : x ≤ y ?< if true = (x < y).
+
+
+Lemma lersifF x y : x ≤ y ?< if false = (x ≤ y).
+
+
+Lemma lersif_oppl b x y : - x ≤ y ?< if b = (- y ≤ x ?< if b).
+
+
+Lemma lersif_oppr b x y : x ≤ - y ?< if b = (y ≤ - x ?< if b).
+
+
+Lemma lersif_0oppr b x : 0 ≤ - x ?< if b = (x ≤ 0 ?< if b).
+
+
+Lemma lersif_oppr0 b x : - x ≤ 0 ?< if b = (0 ≤ x ?< if b).
+
+
+Lemma lersif_opp2 b : {mono -%R : x y /~ x ≤ y ?< if b}.
+
+
+Definition lersif_oppE := (lersif_0oppr, lersif_oppr0, lersif_opp2).
+
+
+Lemma lersif_add2l b x : {mono +%R x : y z / y ≤ z ?< if b}.
+
+
+Lemma lersif_add2r b x : {mono +%R^~ x : y z / y ≤ z ?< if b}.
+
+
+Definition lersif_add2 := (lersif_add2l, lersif_add2r).
+
+
+Lemma lersif_subl_addr b x y z : (x - y ≤ z ?< if b) = (x ≤ z + y ?< if b).
+
+
+Lemma lersif_subr_addr b x y z : (x ≤ y - z ?< if b) = (x + z ≤ y ?< if b).
+
+
+Definition lersif_sub_addr := (lersif_subl_addr, lersif_subr_addr).
+
+
+Lemma lersif_subl_addl b x y z : (x - y ≤ z ?< if b) = (x ≤ y + z ?< if b).
+
+
+Lemma lersif_subr_addl b x y z : (x ≤ y - z ?< if b) = (z + x ≤ y ?< if b).
+
+
+Definition lersif_sub_addl := (lersif_subl_addl, lersif_subr_addl).
+
+
+Lemma lersif_andb x y : {morph lersif x y : p q / p || q >-> p && q}.
+
+
+Lemma lersif_orb x y : {morph lersif x y : p q / p && q >-> p || q}.
+
+
+Lemma lersif_imply b1 b2 r1 r2 :
+ b2 ==> b1 → r1 ≤ r2 ?< if b1 → r1 ≤ r2 ?< if b2.
+
+
+Lemma lersifW b x y : x ≤ y ?< if b → x ≤ y.
+
+
+Lemma ltrW_lersif b x y : x < y → x ≤ y ?< if b.
+
+
+Lemma lersif_pmul2l b x : 0 < x → {mono *%R x : y z / y ≤ z ?< if b}.
+
+
+Lemma lersif_pmul2r b x : 0 < x → {mono *%R^~ x : y z / y ≤ z ?< if b}.
+
+
+Lemma lersif_nmul2l b x : x < 0 → {mono *%R x : y z /~ y ≤ z ?< if b}.
+
+
+Lemma lersif_nmul2r b x : x < 0 → {mono *%R^~ x : y z /~ y ≤ z ?< if b}.
+
+
+Lemma real_lersifN x y b : x \is Num.real → y \is Num.real →
+ x ≤ y ?< if ~~b = ~~ (y ≤ x ?< if b).
+
+
+Lemma real_lersif_norml b x y :
+ x \is Num.real →
+ (`|x| ≤ y ?< if b) = ((- y ≤ x ?< if b) && (x ≤ y ?< if b)).
+
+
+Lemma real_lersif_normr b x y :
+ y \is Num.real →
+ (x ≤ `|y| ?< if b) = ((x ≤ y ?< if b) || (x ≤ - y ?< if b)).
+
+
+Lemma lersif_nnormr b x y : y ≤ 0 ?< if ~~ b → (`|x| ≤ y ?< if b) = false.
+
+
+End LersifPo.
+
+
+Notation "x <= y ?< 'if' b" := (lersif x y b)
+ (at level 70, y at next level,
+ format "x '[hv' <= y '/' ?< 'if' b ']'") : ring_scope.
+
+
+Section LersifOrdered.
+
+
+Variable (R : realDomainType) (b : bool) (x y z e : R).
+
+
+Lemma lersifN : (x ≤ y ?< if ~~ b) = ~~ (y ≤ x ?< if b).
+
+
+Lemma lersif_norml :
+ (`|x| ≤ y ?< if b) = (- y ≤ x ?< if b) && (x ≤ y ?< if b).
+
+
+Lemma lersif_normr :
+ (x ≤ `|y| ?< if b) = (x ≤ y ?< if b) || (x ≤ - y ?< if b).
+
+
+Lemma lersif_distl :
+ (`|x - y| ≤ e ?< if b) = (y - e ≤ x ?< if b) && (x ≤ y + e ?< if b).
+
+
+Lemma lersif_minr :
+ (x ≤ Num.min y z ?< if b) = (x ≤ y ?< if b) && (x ≤ z ?< if b).
+
+
+Lemma lersif_minl :
+ (Num.min y z ≤ x ?< if b) = (y ≤ x ?< if b) || (z ≤ x ?< if b).
+
+
+Lemma lersif_maxr :
+ (x ≤ Num.max y z ?< if b) = (x ≤ y ?< if b) || (x ≤ z ?< if b).
+
+
+Lemma lersif_maxl :
+ (Num.max y z ≤ x ?< if b) = (y ≤ x ?< if b) && (z ≤ x ?< if b).
+
+
+End LersifOrdered.
+
+
+Section LersifField.
+
+
+Variable (F : numFieldType) (b : bool) (z x y : F).
+
+
+Lemma lersif_pdivl_mulr : 0 < z → x ≤ y / z ?< if b = (x × z ≤ y ?< if b).
+
+
+Lemma lersif_pdivr_mulr : 0 < z → y / z ≤ x ?< if b = (y ≤ x × z ?< if b).
+
+
+Lemma lersif_pdivl_mull : 0 < z → x ≤ z^-1 × y ?< if b = (z × x ≤ y ?< if b).
+
+
+Lemma lersif_pdivr_mull : 0 < z → z^-1 × y ≤ x ?< if b = (y ≤ z × x ?< if b).
+
+
+Lemma lersif_ndivl_mulr : z < 0 → x ≤ y / z ?< if b = (y ≤ x × z ?< if b).
+
+
+Lemma lersif_ndivr_mulr : z < 0 → y / z ≤ x ?< if b = (x × z ≤ y ?< if b).
+
+
+Lemma lersif_ndivl_mull : z < 0 → x ≤ z^-1 × y ?< if b = (y ≤z × x ?< if b).
+
+
+Lemma lersif_ndivr_mull : z < 0 → z^-1 × y ≤ x ?< if b = (z × x ≤ y ?< if b).
+
+
+End LersifField.
+
+
+Variant itv_bound (T : Type) : Type := BOpen_if of bool & T | BInfty.
+Notation BOpen := (BOpen_if true).
+Notation BClose := (BOpen_if false).
+Variant interval (T : Type) := Interval of itv_bound T & itv_bound T.
@@ -109,25 +305,81 @@
We provide the 9 following notations to help writing formal intervals
-
Notation "`[ a , b ]" := (
Interval (
BClose a) (
BClose b))
+
Notation "`[ a , b ]" := (
Interval (
BClose a) (
BClose b))
(
at level 0,
a,
b at level 9 ,
format "`[ a , b ]") :
ring_scope.
-
Notation "`] a , b ]" := (
Interval (
BOpen a) (
BClose b))
+
Notation "`] a , b ]" := (
Interval (
BOpen a) (
BClose b))
(
at level 0,
a,
b at level 9 ,
format "`] a , b ]") :
ring_scope.
-
Notation "`[ a , b [" := (
Interval (
BClose a) (
BOpen b))
+
Notation "`[ a , b [" := (
Interval (
BClose a) (
BOpen b))
(
at level 0,
a,
b at level 9 ,
format "`[ a , b [") :
ring_scope.
-
Notation "`] a , b [" := (
Interval (
BOpen a) (
BOpen b))
+
Notation "`] a , b [" := (
Interval (
BOpen a) (
BOpen b))
(
at level 0,
a,
b at level 9 ,
format "`] a , b [") :
ring_scope.
-
Notation "`] '-oo' , b ]" := (
Interval (
BInfty _) (
BClose b))
+
Notation "`] '-oo' , b ]" := (
Interval (
BInfty _) (
BClose b))
(
at level 0,
b at level 9 ,
format "`] '-oo' , b ]") :
ring_scope.
-
Notation "`] '-oo' , b [" := (
Interval (
BInfty _) (
BOpen b))
+
Notation "`] '-oo' , b [" := (
Interval (
BInfty _) (
BOpen b))
(
at level 0,
b at level 9 ,
format "`] '-oo' , b [") :
ring_scope.
-
Notation "`[ a , '+oo' [" := (
Interval (
BClose a) (
BInfty _))
+
Notation "`[ a , '+oo' [" := (
Interval (
BClose a) (
BInfty _))
(
at level 0,
a at level 9 ,
format "`[ a , '+oo' [") :
ring_scope.
-
Notation "`] a , '+oo' [" := (
Interval (
BOpen a) (
BInfty _))
+
Notation "`] a , '+oo' [" := (
Interval (
BOpen a) (
BInfty _))
(
at level 0,
a at level 9 ,
format "`] a , '+oo' [") :
ring_scope.
-
Notation "`] -oo , '+oo' [" := (
Interval (
BInfty _) (
BInfty _))
+
Notation "`] -oo , '+oo' [" := (
Interval (
BInfty _) (
BInfty _))
(
at level 0,
format "`] -oo , '+oo' [") :
ring_scope.
+
+
Section IntervalEq.
+
+
+
Variable T :
eqType.
+
+
+
Definition eq_itv_bound (
b1 b2 :
itv_bound T) :
bool :=
+
match b1,
b2 with
+ |
BOpen_if a x,
BOpen_if b y ⇒
(a == b) && (x == y)
+ |
BInfty,
BInfty ⇒
true
+ |
_,
_ ⇒
false
+
end.
+
+
+
Lemma eq_itv_boundP :
Equality.axiom eq_itv_bound.
+
+
+
Canonical itv_bound_eqMixin :=
EqMixin eq_itv_boundP.
+
Canonical itv_bound_eqType :=
+
Eval hnf in EqType (
itv_bound T)
itv_bound_eqMixin.
+
+
+
Definition eqitv (
x y :
interval T) :
bool :=
+
let:
Interval x x' :=
x in
+
let:
Interval y y' :=
y in (x == y) && (x' == y').
+
+
+
Lemma eqitvP :
Equality.axiom eqitv.
+
+
+
Canonical interval_eqMixin :=
EqMixin eqitvP.
+
Canonical interval_eqType :=
Eval hnf in EqType (
interval T)
interval_eqMixin.
+
+
+
End IntervalEq.
+
+
+
Section IntervalPo.
+
+
+
Variable R :
numDomainType.
+
+
+
Definition pred_of_itv (
i :
interval R) :
pred R :=
+
[pred x | let:
Interval l u :=
i in
+
match l with
+ |
BOpen_if b lb ⇒
lb ≤ x ?< if b
+ |
BInfty ⇒
true
+
end &&
+
match u with
+ |
BOpen_if b ub ⇒
x ≤ ub ?< if b
+ |
BInfty ⇒
true
+
end].
+
Canonical Structure itvPredType :=
PredType pred_of_itv.
+
let: Interval l u := i in
(match l with
- | BClose a ⇒ (a ≤ x) × (x < a = false)
- | BOpen a ⇒ (a ≤ x) × (a < x) × (x ≤ a = false)
- | BInfty ⇒ ∀ x : R, x == x
- end ×
+ | BClose a ⇒ (a ≤ x) × (x < a = false)
+ | BOpen a ⇒ (a ≤ x) × (a < x) × (x ≤ a = false) × (x < a = false)
+ | BInfty ⇒ ∀ x : R, x == x
+ end ×
match u with
- | BClose b ⇒ (x ≤ b) × (b < x = false)
- | BOpen b ⇒ (x ≤ b) × (x < b) × (b ≤ x = false)
- | BInfty ⇒ ∀ x : R, x == x
- end ×
+ | BClose b ⇒ (x ≤ b) × (b < x = false)
+ | BOpen b ⇒ (x ≤ b) × (x < b) × (b ≤ x = false) × (b < x = false)
+ | BInfty ⇒ ∀ x : R, x == x
+ end ×
match l, u with
| BClose a, BClose b ⇒
- (a ≤ b) × (b < a = false) × (a \in `[a, b]) × (b \in `[a, b])
+ (a ≤ b) × (b < a = false) × (a \in `[a, b]) × (b \in `[a, b])
| BClose a, BOpen b ⇒
- (a ≤ b) × (a < b) × (b ≤ a = false)
- × (a \in `[a, b]) × (a \in `[a, b[)* (b \in `[a, b]) × (b \in `]a, b])
+ (a ≤ b) × (a < b) × (b ≤ a = false) × (b < a = false)
+ × (a \in `[a, b]) × (a \in `[a, b[)* (b \in `[a, b]) × (b \in `]a, b])
| BOpen a, BClose b ⇒
- (a ≤ b) × (a < b) × (b ≤ a = false)
- × (a \in `[a, b]) × (a \in `[a, b[)* (b \in `[a, b]) × (b \in `]a, b])
+ (a ≤ b) × (a < b) × (b ≤ a = false) × (b < a = false)
+ × (a \in `[a, b]) × (a \in `[a, b[)* (b \in `[a, b]) × (b \in `]a, b])
| BOpen a, BOpen b ⇒
- (a ≤ b) × (a < b) × (b ≤ a = false)
- × (a \in `[a, b]) × (a \in `[a, b[)* (b \in `[a, b]) × (b \in `]a, b])
- | _, _ ⇒ ∀ x : R, x == x
+ (a ≤ b) × (a < b) × (b ≤ a = false) × (b < a = false)
+ × (a \in `[a, b]) × (a \in `[a, b[)* (b \in `[a, b]) × (b \in `]a, b])
+ | _, _ ⇒ ∀ x : R, x == x
end)%type.
Definition itv_decompose (i : interval R) x : Prop :=
let: Interval l u := i in
- ((match l with
- | BClose a ⇒ (a ≤ x) : Prop
- | BOpen a ⇒ (a < x) : Prop
- | BInfty ⇒ True
- end : Prop) ×
- (match u with
- | BClose b ⇒ (x ≤ b) : Prop
- | BOpen b ⇒ (x < b) : Prop
- | BInfty ⇒ True
- end : Prop))%type.
+ ((match l with
+ | BOpen_if b lb ⇒ (lb ≤ x ?< if b) : Prop
+ | BInfty ⇒ True
+ end : Prop) ×
+ (match u with
+ | BOpen_if b ub ⇒ (x ≤ ub ?< if b) : Prop
+ | BInfty ⇒ True
+ end : Prop))%type.
Lemma itv_dec : ∀ (x : R) (i : interval R),
- reflect (itv_decompose i x) (x \in i).
-
-
-
-
-Definition lersif (x y : R) b := if b then x < y else x ≤ y.
-
-
-
-
-Lemma lersifxx x b: (x ≤ x ?< if b) = ~~ b.
+ reflect (itv_decompose i x) (x \in i).
-Lemma lersif_trans x y z b1 b2 :
- x ≤ y ?< if b1 → y ≤ z ?< if b2 → x ≤ z ?< if b1 || b2.
-Lemma lersifW b x y : x ≤ y ?< if b → x ≤ y.
-
-
-Lemma lersifNF x y b : y ≤ x ?< if ~~ b → x ≤ y ?< if b = false.
-
-
-Lemma lersifS x y b : x < y → x ≤ y ?< if b.
-
-
-Lemma lersifT x y : x ≤ y ?< if true = (x < y).
-
-
-Lemma lersifF x y : x ≤ y ?< if false = (x ≤ y).
-
-
-Definition le_boundl b1 b2 :=
+Definition le_boundl (b1 b2 : itv_bound R) :=
match b1, b2 with
- | BOpen_if b1 x1, BOpen_if b2 x2 ⇒ x1 ≤ x2 ?< if (~~ b2 && b1)
- | BOpen_if _ _, BInfty ⇒ false
- | _, _ ⇒ true
+ | BOpen_if b1 x1, BOpen_if b2 x2 ⇒ x1 ≤ x2 ?< if ~~ b2 && b1
+ | BOpen_if _ _, BInfty ⇒ false
+ | _, _ ⇒ true
end.
-Definition le_boundr b1 b2 :=
+Definition le_boundr (b1 b2 : itv_bound R) :=
match b1, b2 with
- | BOpen_if b1 x1, BOpen_if b2 x2 ⇒ x1 ≤ x2 ?< if (~~ b1 && b2)
- | BInfty, BOpen_if _ _ ⇒ false
- | _, _ ⇒ true
+ | BOpen_if b1 x1, BOpen_if b2 x2 ⇒ x1 ≤ x2 ?< if ~~ b1 && b2
+ | BInfty, BOpen_if _ _ ⇒ false
+ | _, _ ⇒ true
end.
Lemma itv_boundlr bl br x :
- (x \in Interval bl br) =
- (le_boundl bl (BClose x)) && (le_boundr (BClose x) br).
+ (x \in Interval bl br) =
+ (le_boundl bl (BClose x)) && (le_boundr (BClose x) br).
-Lemma le_boundr_refl : reflexive le_boundr.
+Lemma le_boundl_refl : reflexive le_boundl.
-Hint Resolve le_boundr_refl.
+Hint Resolve le_boundl_refl : core.
-Lemma le_boundl_refl : reflexive le_boundl.
+Lemma le_boundr_refl : reflexive le_boundr.
-Hint Resolve le_boundl_refl.
+Hint Resolve le_boundr_refl : core.
+
+
+Lemma le_boundl_trans : transitive le_boundl.
+
+
+Lemma le_boundr_trans : transitive le_boundr.
Lemma le_boundl_bb x b1 b2 :
- le_boundl (BOpen_if b1 x) (BOpen_if b2 x) = (b1 ==> b2).
+ le_boundl (BOpen_if b1 x) (BOpen_if b2 x) = (b1 ==> b2).
Lemma le_boundr_bb x b1 b2 :
- le_boundr (BOpen_if b1 x) (BOpen_if b2 x) = (b2 ==> b1).
+ le_boundr (BOpen_if b1 x) (BOpen_if b2 x) = (b2 ==> b1).
+
+
+Lemma le_boundl_anti b1 b2 : (le_boundl b1 b2 && le_boundl b2 b1) = (b1 == b2).
+
+
+Lemma le_boundr_anti b1 b2 : (le_boundr b1 b2 && le_boundr b2 b1) = (b1 == b2).
Lemma itv_xx x bl br :
- Interval (BOpen_if bl x) (BOpen_if br x) =i
- if ~~ (bl || br) then pred1 x else pred0.
-
+ Interval (BOpen_if bl x) (BOpen_if br x) =i
+ if ~~ (bl || br) then pred1 x else pred0.
+
-Lemma itv_gte ba xa bb xb : xb ≤ xa ?< if ~~ (ba || bb)
- → Interval (BOpen_if ba xa) (BOpen_if bb xb) =i pred0.
+Lemma itv_gte ba xa bb xb : xb ≤ xa ?< if ~~ (ba || bb)
+ → Interval (BOpen_if ba xa) (BOpen_if bb xb) =i pred0.
Lemma boundl_in_itv : ∀ ba xa b,
- xa \in Interval (BOpen_if ba xa) b =
- if ba then false else le_boundr (BClose xa) b.
+ xa \in Interval (BOpen_if ba xa) b =
+ if ba then false else le_boundr (BClose xa) b.
Lemma boundr_in_itv : ∀ bb xb a,
- xb \in Interval a (BOpen_if bb xb) =
- if bb then false else le_boundl a (BClose xb).
+ xb \in Interval a (BOpen_if bb xb) =
+ if bb then false else le_boundl a (BClose xb).
-Definition bound_in_itv := (boundl_in_itv, boundr_in_itv).
+Definition bound_in_itv := (boundl_in_itv, boundr_in_itv).
-Lemma itvP : ∀ (x : R) (i : interval R), (x \in i) → itv_rewrite i x.
+Lemma itvP : ∀ (x : R) (i : interval R), x \in i → itv_rewrite i x.
-Hint Rewrite intP.
+
+Definition itv_intersection (x y : interval R) : interval R :=
+ let: Interval x x' := x in
+ let: Interval y y' := y in
+ Interval
+ (if le_boundl x y then y else x)
+ (if le_boundr x' y' then x' else y').
+
+
+Definition itv_intersection1i : left_id `]-oo, +oo[ itv_intersection.
+
+
+Definition itv_intersectioni1 : right_id `]-oo, +oo[ itv_intersection.
+
+
+Lemma itv_intersectionii : idempotent itv_intersection.
+
Definition subitv (i1 i2 : interval R) :=
match i1, i2 with
- | Interval a1 b1, Interval a2 b2 ⇒ le_boundl a2 a1 && le_boundr b1 b2
+ | Interval a1 b1, Interval a2 b2 ⇒ le_boundl a2 a1 && le_boundr b1 b2
end.
-Lemma subitvP : ∀ (i2 i1 : interval R),
- (subitv i1 i2) → {subset i1 ≤ i2}.
+Lemma subitvP : ∀ (i2 i1 : interval R), subitv i1 i2 → {subset i1 ≤ i2}.
-Lemma subitvPr : ∀ (a b1 b2 : itv_bound R),
- le_boundr b1 b2 → {subset (Interval a b1) ≤ (Interval a b2)}.
+Lemma subitvPr (a b1 b2 : itv_bound R) :
+ le_boundr b1 b2 → {subset (Interval a b1) ≤ (Interval a b2)}.
-Lemma subitvPl : ∀ (a1 a2 b : itv_bound R),
- le_boundl a2 a1 → {subset (Interval a1 b) ≤ (Interval a2 b)}.
+Lemma subitvPl (a1 a2 b : itv_bound R) :
+ le_boundl a2 a1 → {subset (Interval a1 b) ≤ (Interval a2 b)}.
-Lemma lersif_in_itv : ∀ ba bb xa xb x,
- x \in Interval (BOpen_if ba xa) (BOpen_if bb xb) →
- xa ≤ xb ?< if ba || bb.
-
-
-Lemma ltr_in_itv : ∀ ba bb xa xb x, ba || bb →
- x \in Interval (BOpen_if ba xa) (BOpen_if bb xb) → xa < xb.
-
+Lemma lersif_in_itv ba bb xa xb x :
+ x \in Interval (BOpen_if ba xa) (BOpen_if bb xb) →
+ xa ≤ xb ?< if ba || bb.
+
-Lemma ler_in_itv : ∀ ba bb xa xb x,
- x \in Interval (BOpen_if ba xa) (BOpen_if bb xb) → xa ≤ xb.
+Lemma ltr_in_itv ba bb xa xb x :
+ ba || bb → x \in Interval (BOpen_if ba xa) (BOpen_if bb xb) → xa < xb.
-Lemma mem0_itvcc_xNx : ∀ x, (0 \in `[-x, x]) = (0 ≤ x).
-
+Lemma ler_in_itv ba bb xa xb x :
+ x \in Interval (BOpen_if ba xa) (BOpen_if bb xb) → xa ≤ xb.
+
-Lemma mem0_itvoo_xNx : ∀ x, 0 \in `](-x), x[ = (0 < x).
-
+Lemma mem0_itvcc_xNx x : (0 \in `[-x, x]) = (0 ≤ x).
+
-Lemma itv_splitI : ∀ a b, ∀ x,
- x \in Interval a b = (x \in Interval a (BInfty _)) && (x \in Interval (BInfty _) b).
+Lemma mem0_itvoo_xNx x : 0 \in `](-x), x[ = (0 < x).
-Lemma real_lersifN x y b : x \in Num.real → y \in Num.real →
- x ≤ y ?< if ~~b = ~~ (y ≤ x ?< if b).
+Lemma itv_splitI : ∀ a b x,
+ x \in Interval a b =
+ (x \in Interval a (BInfty _)) && (x \in Interval (BInfty _) b).
Lemma oppr_itv ba bb (xa xb x : R) :
- (-x \in Interval (BOpen_if ba xa) (BOpen_if bb xb)) =
- (x \in Interval (BOpen_if bb (-xb)) (BOpen_if ba (-xa))).
+ (-x \in Interval (BOpen_if ba xa) (BOpen_if bb xb)) =
+ (x \in Interval (BOpen_if bb (-xb)) (BOpen_if ba (-xa))).
-Lemma oppr_itvoo (a b x : R) : (-x \in `]a, b[) = (x \in `](-b), (-a)[).
+Lemma oppr_itvoo (a b x : R) : (-x \in `]a, b[) = (x \in `](-b), (-a)[).
-Lemma oppr_itvco (a b x : R) : (-x \in `[a, b[) = (x \in `](-b), (-a)]).
+Lemma oppr_itvco (a b x : R) : (-x \in `[a, b[) = (x \in `](-b), (-a)]).
-Lemma oppr_itvoc (a b x : R) : (-x \in `]a, b]) = (x \in `[(-b), (-a)[).
+Lemma oppr_itvoc (a b x : R) : (-x \in `]a, b]) = (x \in `[(-b), (-a)[).
-Lemma oppr_itvcc (a b x : R) : (-x \in `[a, b]) = (x \in `[(-b), (-a)]).
+Lemma oppr_itvcc (a b x : R) : (-x \in `[a, b]) = (x \in `[(-b), (-a)]).
End IntervalPo.
-Notation BOpen := (BOpen_if true).
-Notation BClose := (BOpen_if false).
-Notation "`[ a , b ]" := (Interval (BClose a) (BClose b))
- (at level 0, a, b at level 9 , format "`[ a , b ]") : ring_scope.
-Notation "`] a , b ]" := (Interval (BOpen a) (BClose b))
- (at level 0, a, b at level 9 , format "`] a , b ]") : ring_scope.
-Notation "`[ a , b [" := (Interval (BClose a) (BOpen b))
- (at level 0, a, b at level 9 , format "`[ a , b [") : ring_scope.
-Notation "`] a , b [" := (Interval (BOpen a) (BOpen b))
- (at level 0, a, b at level 9 , format "`] a , b [") : ring_scope.
-Notation "`] '-oo' , b ]" := (Interval (BInfty _) (BClose b))
- (at level 0, b at level 9 , format "`] '-oo' , b ]") : ring_scope.
-Notation "`] '-oo' , b [" := (Interval (BInfty _) (BOpen b))
- (at level 0, b at level 9 , format "`] '-oo' , b [") : ring_scope.
-Notation "`[ a , '+oo' [" := (Interval (BClose a) (BInfty _))
- (at level 0, a at level 9 , format "`[ a , '+oo' [") : ring_scope.
-Notation "`] a , '+oo' [" := (Interval (BOpen a) (BInfty _))
- (at level 0, a at level 9 , format "`] a , '+oo' [") : ring_scope.
-Notation "`] -oo , '+oo' [" := (Interval (BInfty _) (BInfty _))
- (at level 0, format "`] -oo , '+oo' [") : ring_scope.
+Section IntervalOrdered.
-Notation "x <= y ?< 'if' b" := (lersif x y b)
- (at level 70, y at next level,
- format "x '[hv' <= y '/' ?< 'if' b ']'") : ring_scope.
+Variable R : realDomainType.
-Section IntervalOrdered.
+Lemma le_boundl_total : total (@le_boundl R).
+
+
+Lemma le_boundr_total : total (@le_boundr R).
+
+
+Lemma itv_splitU (xc : R) bc a b : xc \in Interval a b →
+ ∀ y, y \in Interval a b =
+ (y \in Interval a (BOpen_if (~~ bc) xc))
+ || (y \in Interval (BOpen_if bc xc) b).
-Variable R : realDomainType.
+Lemma itv_splitU2 (x : R) a b : x \in Interval a b →
+ ∀ y, y \in Interval a b =
+ [|| (y \in Interval a (BOpen x)), (y == x)
+ | (y \in Interval (BOpen x) b)].
-Lemma lersifN (x y : R) b : (x ≤ y ?< if ~~ b) = ~~ (y ≤ x ?< if b).
-
+Lemma itv_intersectionC : commutative (@itv_intersection R).
+
+
+Lemma itv_intersectionA : associative (@itv_intersection R).
+
-Lemma itv_splitU (xc : R) bc a b : xc \in Interval a b →
- ∀ y, y \in Interval a b =
- (y \in Interval a (BOpen_if (~~ bc) xc))
- || (y \in Interval (BOpen_if bc xc) b).
+Canonical itv_intersection_monoid :=
+ Monoid.Law itv_intersectionA (@itv_intersection1i R) (@itv_intersectioni1 R).
-Lemma itv_splitU2 (x : R) a b : x \in Interval a b →
- ∀ y, y \in Interval a b =
- [|| (y \in Interval a (BOpen x)), (y == x)
- | (y \in Interval (BOpen x) b)].
+Canonical itv_intersection_comoid := Monoid.ComLaw itv_intersectionC.
End IntervalOrdered.
@@ -401,14 +637,14 @@
Variable R : realFieldType.
-Lemma mid_in_itv : ∀ ba bb (xa xb : R), xa ≤ xb ?< if (ba || bb)
- → mid xa xb \in Interval (BOpen_if ba xa) (BOpen_if bb xb).
+Lemma mid_in_itv : ∀ ba bb (xa xb : R), xa ≤ xb ?< if ba || bb
+ → mid xa xb \in Interval (BOpen_if ba xa) (BOpen_if bb xb).
-Lemma mid_in_itvoo : ∀ (xa xb : R), xa < xb → mid xa xb \in `]xa, xb[.
+Lemma mid_in_itvoo : ∀ (xa xb : R), xa < xb → mid xa xb \in `]xa, xb[.
-Lemma mid_in_itvcc : ∀ (xa xb : R), xa ≤ xb → mid xa xb \in `[xa, xb].
+Lemma mid_in_itvcc : ∀ (xa xb : R), xa ≤ xb → mid xa xb \in `[xa, xb].
End IntervalField.
--
cgit v1.2.3