Library mathcomp.analysis.set_interval
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
From mathcomp Require Import finmap fingroup perm rat.
Require Import boolp reals ereal classical_sets signed topology.
Require Import mathcomp_extra functions normedtype.
From HB Require Import structures.
Require Import sequences.
From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
From mathcomp Require Import finmap fingroup perm rat.
Require Import boolp reals ereal classical_sets signed topology.
Require Import mathcomp_extra functions normedtype.
From HB Require Import structures.
Require Import sequences.
This files contains lemmas about sets and intervals.
neitv i == the interval i is non-empty
when the support type is a numFieldType, this
is equivalent to (i.1 < i.2)%O (lemma neitvE)
set_itv_infty_set0 == multirule to simplify empty intervals
set_itvE == multirule to turn intervals into inequalities
conv, ndconv == convexity operator
factor a b x := (x - a) / (b - a)
disjoint_itv i j == intervals i and j are disjoint
Set Implicit Arguments.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldTopology.Exports.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
definitions and lemmas to make a bridge between MathComp intervals and
classical sets
Section set_itv_porderType.
Variables (d : unit) (T : porderType d).
Implicit Types (i j : interval T) (x y : T) (a : itv_bound T).
Definition neitv i := [set` i] != set0.
Lemma neitv_lt_bnd i : neitv i → (i.1 < i.2)%O.
Lemma set_itvP i j : [set` i] = [set` j] :> set _ ↔ i =i j.
Lemma subset_itvP i j : {subset i ≤ j} ↔ [set` i] `<=` [set` j].
Lemma set_itvoo x y : `]x, y[%classic = [set z | (x < z < y)%O].
Lemma set_itvco x y : `[x, y[%classic = [set z | (x ≤ z < y)%O].
Lemma set_itvcc x y : `[x, y]%classic = [set z | (x ≤ z ≤ y)%O].
Lemma set_itvoc x y : `]x, y]%classic = [set z | (x < z ≤ y)%O].
Lemma set_itv1 x : `[x, x]%classic = [set x].
Lemma set_itvoo0 x : `]x, x[%classic = set0.
Lemma set_itvoc0 x : `]x, x]%classic = set0.
Lemma set_itvco0 x : `[x, x[%classic = set0.
Lemma set_itv_infty_infty : `]-oo, +oo[%classic = @setT T.
Lemma set_itv_o_infty x : `]x, +oo[%classic = [set z | (x < z)%O].
Lemma set_itv_c_infty x : `[x, +oo[%classic = [set z | (x ≤ z)%O].
Lemma set_itv_infty_o x : `]-oo, x[%classic = [set z | (z < x)%O].
Lemma set_itv_infty_c x : `]-oo, x]%classic = [set z | (z ≤ x)%O].
Lemma set_itv_pinfty_bnd a : [set` Interval +oo%O a] = set0.
Lemma set_itv_bnd_ninfty a : [set` Interval a -oo%O] = set0.
Definition set_itv_infty_set0 := (set_itv_bnd_ninfty, set_itv_pinfty_bnd).
Definition set_itvE := (set_itv1, set_itvoo0, set_itvoc0, set_itvco0, set_itvoo,
set_itvcc, set_itvoc, set_itvco, set_itv_infty_infty, set_itv_o_infty,
set_itv_c_infty, set_itv_infty_o, set_itv_infty_c, set_itv_infty_set0).
Lemma setUitv1 (a : itv_bound T) (x : T) : (a ≤ BLeft x)%O →
[set` Interval a (BLeft x)] `|` [set x] = [set` Interval a (BRight x)].
Lemma setU1itv (a : itv_bound T) (x : T) : (BRight x ≤ a)%O →
x |` [set` Interval (BRight x) a] = [set` Interval (BLeft x) a].
End set_itv_porderType.
Arguments neitv {d T} _.
Section set_itv_latticeType.
Variables (d : unit) (T : latticeType d).
Implicit Types (i j : interval T) (x y : T) (a : itv_bound T).
Lemma set_itvI i j : [set` (i `&` j)%O] = [set` i] `&` [set` j].
End set_itv_latticeType.
Section set_itv_numFieldType.
Variable R : numFieldType.
Implicit Types i : interval R.
Lemma neitvE i : neitv i = (i.1 < i.2)%O.
Lemma neitvP i : reflect (i.1 < i.2)%O (neitv i).
End set_itv_numFieldType.
Lemma setitv0 (R : realDomainType) : [set` (0%O : interval R)] = set0.
Section interval_has_bound.
Variable R : numDomainType.
Lemma has_lbound_itv (x : R) b (a : itv_bound R) :
has_lbound [set` Interval (BSide b x) a].
Lemma has_ubound_itv (x : R) b (a : itv_bound R) :
has_ubound [set` Interval a (BSide b x)].
End interval_has_bound.
Section interval_hasNbound.
Variable R : realDomainType.
Lemma hasNlbound_itv (a : itv_bound R) : a != -oo%O →
¬ has_lbound [set` Interval -oo%O a].
Lemma hasNubound_itv (a : itv_bound R) : a != +oo%O →
¬ has_ubound [set` Interval a +oo%O].
End interval_hasNbound.
#[global] Hint Extern 0 (has_lbound _) ⇒ solve[apply: has_lbound_itv] : core.
#[global] Hint Extern 0 (has_ubound _) ⇒ solve[apply: has_ubound_itv] : core.
#[global]
Hint Extern 0 (¬ has_lbound _) ⇒ solve[by apply: hasNlbound_itv] : core.
#[global]
Hint Extern 0 (¬ has_ubound _) ⇒ solve[by apply: hasNubound_itv] : core.
Section interval_has.
Variable R : realType.
Implicit Types x : R.
Lemma has_sup_half x b (i : itv_bound R) : (i < BSide b x)%O →
has_sup [set` Interval i (BSide b x)].
Lemma has_inf_half x b (i : itv_bound R) : (BSide b x < i)%O →
has_inf [set` Interval (BSide b x) i].
End interval_has.
#[global]
Hint Extern 0 (has_sup _) ⇒ solve[apply: has_sup1 | exact: has_sup_half] : core.
#[global]
Hint Extern 0 (has_inf _) ⇒ solve[apply: has_inf1 | exact: has_inf_half]: core.
Lemma opp_itv_bnd_infty (R : numDomainType) (x : R) b :
-%R @` [set` Interval (BSide b x) +oo%O] =
[set` Interval -oo%O (BSide (negb b) (- x))].
Lemma opp_itv_infty_bnd (R : numDomainType) (x : R) b :
-%R @` [set` Interval -oo%O (BSide b x)] =
[set` Interval (BSide (negb b) (- x)) +oo%O].
Lemma opp_itv_bnd_bnd (R : numDomainType) a b (x y : R) :
-%R @` [set` Interval (BSide a x) (BSide b y)] =
[set` Interval (BSide (~~ b) (- y)) (BSide (~~ a) (- x))].
Section interval_sup_inf.
Variable R : realType.
Implicit Types x y : R.
Let sup_itv_infty_bnd x b : sup [set` Interval -oo%O (BSide b x)] = x.
Let inf_itv_bnd_infty x b : inf [set` Interval (BSide b x) +oo%O] = x.
Let sup_itv_o_bnd x y b : x < y →
sup [set` Interval (BRight x) (BSide b y)] = y.
Let sup_itv_bounded x y a b : (BSide a x < BSide b y)%O →
sup [set` Interval (BSide a x) (BSide b y)] = y.
Let inf_itv_bnd_o x y b : (BSide b x < BLeft y)%O →
inf [set` Interval (BSide b x) (BLeft y)] = x.
Let inf_itv_bounded x y a b : (BSide a x < BSide b y)%O →
inf [set` Interval (BSide a x) (BSide b y)] = x.
Lemma sup_itv a b x : (a < BSide b x)%O →
sup [set` Interval a (BSide b x)] = x.
Lemma inf_itv a b x : (BSide b x < a)%O →
inf [set` Interval (BSide b x) a] = x.
Lemma sup_itvcc x y : x ≤ y → sup `[x, y] = y.
Lemma inf_itvcc x y : x ≤ y → inf `[x, y] = x.
End interval_sup_inf.
Variables (d : unit) (T : porderType d).
Implicit Types (i j : interval T) (x y : T) (a : itv_bound T).
Definition neitv i := [set` i] != set0.
Lemma neitv_lt_bnd i : neitv i → (i.1 < i.2)%O.
Lemma set_itvP i j : [set` i] = [set` j] :> set _ ↔ i =i j.
Lemma subset_itvP i j : {subset i ≤ j} ↔ [set` i] `<=` [set` j].
Lemma set_itvoo x y : `]x, y[%classic = [set z | (x < z < y)%O].
Lemma set_itvco x y : `[x, y[%classic = [set z | (x ≤ z < y)%O].
Lemma set_itvcc x y : `[x, y]%classic = [set z | (x ≤ z ≤ y)%O].
Lemma set_itvoc x y : `]x, y]%classic = [set z | (x < z ≤ y)%O].
Lemma set_itv1 x : `[x, x]%classic = [set x].
Lemma set_itvoo0 x : `]x, x[%classic = set0.
Lemma set_itvoc0 x : `]x, x]%classic = set0.
Lemma set_itvco0 x : `[x, x[%classic = set0.
Lemma set_itv_infty_infty : `]-oo, +oo[%classic = @setT T.
Lemma set_itv_o_infty x : `]x, +oo[%classic = [set z | (x < z)%O].
Lemma set_itv_c_infty x : `[x, +oo[%classic = [set z | (x ≤ z)%O].
Lemma set_itv_infty_o x : `]-oo, x[%classic = [set z | (z < x)%O].
Lemma set_itv_infty_c x : `]-oo, x]%classic = [set z | (z ≤ x)%O].
Lemma set_itv_pinfty_bnd a : [set` Interval +oo%O a] = set0.
Lemma set_itv_bnd_ninfty a : [set` Interval a -oo%O] = set0.
Definition set_itv_infty_set0 := (set_itv_bnd_ninfty, set_itv_pinfty_bnd).
Definition set_itvE := (set_itv1, set_itvoo0, set_itvoc0, set_itvco0, set_itvoo,
set_itvcc, set_itvoc, set_itvco, set_itv_infty_infty, set_itv_o_infty,
set_itv_c_infty, set_itv_infty_o, set_itv_infty_c, set_itv_infty_set0).
Lemma setUitv1 (a : itv_bound T) (x : T) : (a ≤ BLeft x)%O →
[set` Interval a (BLeft x)] `|` [set x] = [set` Interval a (BRight x)].
Lemma setU1itv (a : itv_bound T) (x : T) : (BRight x ≤ a)%O →
x |` [set` Interval (BRight x) a] = [set` Interval (BLeft x) a].
End set_itv_porderType.
Arguments neitv {d T} _.
Section set_itv_latticeType.
Variables (d : unit) (T : latticeType d).
Implicit Types (i j : interval T) (x y : T) (a : itv_bound T).
Lemma set_itvI i j : [set` (i `&` j)%O] = [set` i] `&` [set` j].
End set_itv_latticeType.
Section set_itv_numFieldType.
Variable R : numFieldType.
Implicit Types i : interval R.
Lemma neitvE i : neitv i = (i.1 < i.2)%O.
Lemma neitvP i : reflect (i.1 < i.2)%O (neitv i).
End set_itv_numFieldType.
Lemma setitv0 (R : realDomainType) : [set` (0%O : interval R)] = set0.
Section interval_has_bound.
Variable R : numDomainType.
Lemma has_lbound_itv (x : R) b (a : itv_bound R) :
has_lbound [set` Interval (BSide b x) a].
Lemma has_ubound_itv (x : R) b (a : itv_bound R) :
has_ubound [set` Interval a (BSide b x)].
End interval_has_bound.
Section interval_hasNbound.
Variable R : realDomainType.
Lemma hasNlbound_itv (a : itv_bound R) : a != -oo%O →
¬ has_lbound [set` Interval -oo%O a].
Lemma hasNubound_itv (a : itv_bound R) : a != +oo%O →
¬ has_ubound [set` Interval a +oo%O].
End interval_hasNbound.
#[global] Hint Extern 0 (has_lbound _) ⇒ solve[apply: has_lbound_itv] : core.
#[global] Hint Extern 0 (has_ubound _) ⇒ solve[apply: has_ubound_itv] : core.
#[global]
Hint Extern 0 (¬ has_lbound _) ⇒ solve[by apply: hasNlbound_itv] : core.
#[global]
Hint Extern 0 (¬ has_ubound _) ⇒ solve[by apply: hasNubound_itv] : core.
Section interval_has.
Variable R : realType.
Implicit Types x : R.
Lemma has_sup_half x b (i : itv_bound R) : (i < BSide b x)%O →
has_sup [set` Interval i (BSide b x)].
Lemma has_inf_half x b (i : itv_bound R) : (BSide b x < i)%O →
has_inf [set` Interval (BSide b x) i].
End interval_has.
#[global]
Hint Extern 0 (has_sup _) ⇒ solve[apply: has_sup1 | exact: has_sup_half] : core.
#[global]
Hint Extern 0 (has_inf _) ⇒ solve[apply: has_inf1 | exact: has_inf_half]: core.
Lemma opp_itv_bnd_infty (R : numDomainType) (x : R) b :
-%R @` [set` Interval (BSide b x) +oo%O] =
[set` Interval -oo%O (BSide (negb b) (- x))].
Lemma opp_itv_infty_bnd (R : numDomainType) (x : R) b :
-%R @` [set` Interval -oo%O (BSide b x)] =
[set` Interval (BSide (negb b) (- x)) +oo%O].
Lemma opp_itv_bnd_bnd (R : numDomainType) a b (x y : R) :
-%R @` [set` Interval (BSide a x) (BSide b y)] =
[set` Interval (BSide (~~ b) (- y)) (BSide (~~ a) (- x))].
Section interval_sup_inf.
Variable R : realType.
Implicit Types x y : R.
Let sup_itv_infty_bnd x b : sup [set` Interval -oo%O (BSide b x)] = x.
Let inf_itv_bnd_infty x b : inf [set` Interval (BSide b x) +oo%O] = x.
Let sup_itv_o_bnd x y b : x < y →
sup [set` Interval (BRight x) (BSide b y)] = y.
Let sup_itv_bounded x y a b : (BSide a x < BSide b y)%O →
sup [set` Interval (BSide a x) (BSide b y)] = y.
Let inf_itv_bnd_o x y b : (BSide b x < BLeft y)%O →
inf [set` Interval (BSide b x) (BLeft y)] = x.
Let inf_itv_bounded x y a b : (BSide a x < BSide b y)%O →
inf [set` Interval (BSide a x) (BSide b y)] = x.
Lemma sup_itv a b x : (a < BSide b x)%O →
sup [set` Interval a (BSide b x)] = x.
Lemma inf_itv a b x : (BSide b x < a)%O →
inf [set` Interval (BSide b x) a] = x.
Lemma sup_itvcc x y : x ≤ y → sup `[x, y] = y.
Lemma inf_itvcc x y : x ≤ y → inf `[x, y] = x.
End interval_sup_inf.
lemmas between itv and set-theoretic operations
Section set_itv_porderType.
Variables (d : unit) (T : orderType d).
Implicit Types (a : itv_bound T) (x y : T) (i j : interval T) (b : bool).
Lemma setCitvl a : ~` [set` Interval -oo%O a] = [set` Interval a +oo%O].
Lemma setCitvr a : ~` [set` Interval a +oo%O] = [set` Interval -oo%O a].
Lemma set_itv_splitI i : [set` i] = [set` Interval i.1 +oo%O] `&` [set` Interval -oo%O i.2].
Lemma setCitv i :
~` [set` i] = [set` Interval -oo%O i.1] `|` [set` Interval i.2 +oo%O].
Lemma set_itv_splitD i :
[set` i] = [set` Interval i.1 +oo%O] `\` [set` Interval i.2 +oo%O].
End set_itv_porderType.
Section set_itv_realType.
Variable R : realType.
Implicit Types x : R.
Lemma set_itvK : {in neitv, cancel pred_set (@Rhull R)}.
Lemma RhullT : Rhull setT = `]-oo, +oo[%R :> interval R.
Lemma RhullK : {in (@is_interval _ : set (set R)), cancel (@Rhull R) pred_set}.
Lemma itv_c_inftyEbigcap x :
`[x, +oo[%classic = \bigcap_k `]x - k.+1%:R^-1, +oo[%classic.
Lemma itv_bnd_inftyEbigcup b x : [set` Interval (BSide b x) +oo%O] =
\bigcup_k [set` Interval (BSide b x) (BLeft k%:R)].
Lemma itv_o_inftyEbigcup x :
`]x, +oo[%classic = \bigcup_k `[x + k.+1%:R^-1, +oo[%classic.
Lemma set_itv_setT (i : interval R) : [set` i] = setT → i = `]-oo, +oo[.
End set_itv_realType.
Lemma set_itv_ge [disp : unit] [T : porderType disp] [b1 b2 : itv_bound T] :
~~ (b1 < b2)%O → [set` Interval b1 b2] = set0.
Section conv_factor_numDomainType.
Variable R : numDomainType.
Implicit Types (a b t r : R) (A : set R).
Lemma mem_1B_itvcc t : (1 - t \in `[0, 1]) = (t \in `[0, 1]).
Definition conv a b t : R := (1 - t) × a + t × b.
Lemma conv_id : conv 0 1 = id.
Lemma convEl a b t : conv a b t = t × (b - a) + a.
Lemma convEr a b t : conv a b t = (1 - t) × (a - b) + b.
Lemma conv10 t : conv 1 0 t = 1 - t.
Lemma conv0 a b : conv a b 0 = a.
Lemma conv1 a b : conv a b 1 = b.
Lemma conv_sym a b t : conv a b t = conv b a (1 - t).
Lemma conv_flat a : conv a a = cst a.
Lemma leW_conv a b : a ≤ b → {homo conv a b : x y / x ≤ y}.
Definition factor a b x := (x - a) / (b - a).
Lemma leW_factor a b : a ≤ b → {homo factor a b : x y / x ≤ y}.
Lemma factor_flat a : factor a a = cst 0.
Lemma factorl a b : factor a b a = 0.
Definition ndconv a b of a < b := conv a b.
Lemma ndconvE a b (ab : a < b) : ndconv ab = conv a b.
End conv_factor_numDomainType.
Section conv_factor_numFieldType.
Variable R : numFieldType.
Implicit Types (a b t r : R) (A : set R).
Lemma factorr a b : a != b → factor a b b = 1.
Lemma factorK a b : a != b → cancel (factor a b) (conv a b).
Lemma convK a b : a != b → cancel (conv a b) (factor a b).
Lemma conv_inj a b : a != b → injective (conv a b).
Lemma factor_inj a b : a != b → injective (factor a b).
Lemma conv_bij a b : a != b → bijective (conv a b).
Lemma factor_bij a b : a != b → bijective (factor a b).
Lemma le_conv a b : a < b → {mono conv a b : x y / x ≤ y}.
Lemma le_factor a b : a < b → {mono factor a b : x y / x ≤ y}.
Lemma lt_conv a b : a < b → {mono conv a b : x y / x < y}.
Lemma lt_factor a b : a < b → {mono factor a b : x y / x < y}.
Let ltNeq a b : a < b → a != b.
Lemma conv_itv_bij ba bb a b : a < b →
set_bij [set` Interval (BSide ba 0) (BSide bb 1)]
[set` Interval (BSide ba a) (BSide bb b)] (conv a b).
Lemma factor_itv_bij ba bb a b : a < b →
set_bij [set` Interval (BSide ba a) (BSide bb b)]
[set` Interval (BSide ba 0) (BSide bb 1)] (factor a b).
Lemma mem_conv_itv ba bb a b : a < b →
set_fun [set` Interval (BSide ba 0) (BSide bb 1)]
[set` Interval (BSide ba a) (BSide bb b)] (conv a b).
Lemma mem_conv_itvcc a b : a ≤ b → set_fun `[0, 1] `[a, b] (conv a b).
Lemma range_conv ba bb a b : a < b →
conv a b @` [set` Interval (BSide ba 0) (BSide bb 1)] =
[set` Interval (BSide ba a) (BSide bb b)].
Lemma range_factor ba bb a b : a < b →
factor a b @` [set` Interval (BSide ba a) (BSide bb b)] =
[set` Interval (BSide ba 0) (BSide bb 1)].
End conv_factor_numFieldType.
Lemma mem_factor_itv (R : realFieldType) ba bb (a b : R) :
set_fun [set` Interval (BSide ba a) (BSide bb b)]
[set` Interval (BSide ba 0) (BSide bb 1)] (factor a b).
Section Rhull_lemmas.
Variable R : realType.
Implicit Types (a b t r : R) (A : set R).
Lemma Rhull_smallest A : [set` Rhull A] = smallest (@is_interval R) A.
Lemma le_Rhull : {homo (@Rhull R) : A B / (A `<=` B) >-> {subset A ≤ B}}.
Lemma neitv_Rhull A : ~~ neitv (Rhull A) → A = set0.
Lemma Rhull_involutive A : Rhull [set` Rhull A] = Rhull A.
End Rhull_lemmas.
Coercion ereal_of_itv_bound T (b : itv_bound T) : \bar T :=
match b with BSide _ y ⇒ y%:E | +oo%O ⇒ +oo%E | -oo%O ⇒ -oo%E end.
Arguments ereal_of_itv_bound T !b.
Lemma le_bnd_ereal (R : realDomainType) (a b : itv_bound R) :
(a ≤ b)%O → (a ≤ b)%E.
Lemma lt_ereal_bnd (R : realDomainType) (a b : itv_bound R) :
(a < b)%E → (a < b)%O.
Lemma neitv_bnd1 (R : numFieldType) (s : seq (interval R)) :
all neitv s → ∀ i, i \in s → i.1 != +oo%O.
Lemma neitv_bnd2 (R : numFieldType) (s : seq (interval R)) :
all neitv s → ∀ i, i \in s → i.2 != -oo%O.
Lemma Interval_ereal_mem (R : realDomainType) (r : R) (a b : itv_bound R) :
r \in Interval a b → (a ≤ r%:E ≤ b)%E.
Lemma ereal_mem_Interval (R : realDomainType) (r : R) (a b : itv_bound R) :
(a < r%:E < b)%E → r \in Interval a b.
Lemma trivIset_set_itv_nth (R : numDomainType) def (s : seq (interval R))
(D : set nat) : [set` def] = set0 →
trivIset D (fun i ⇒ [set` nth def s i]) ↔
trivIset D (fun i ⇒ nth set0 [seq [set` j] | j <- s] i).
Arguments trivIset_set_itv_nth {R} _ {s}.
Section disjoint_itv.
Context {R : numDomainType}.
Definition disjoint_itv : rel (interval R) :=
fun a b ⇒ [disjoint [set` a] & [set` b]].
Lemma disjoint_itvxx (i : interval R) : neitv i → ~~ disjoint_itv i i.
Lemma lt_disjoint (i j : interval R) :
(∀ x y, x \in i → y \in j → x < y) → disjoint_itv i j.
End disjoint_itv.
Lemma disjoint_neitv {R : realFieldType} (i j : interval R) :
disjoint_itv i j ↔ ~~ neitv (itv_meet i j).
Lemma disj_itv_Rhull {R : realType} (A B : set R) : A `&` B = set0 →
is_interval A → is_interval B → disjoint_itv (Rhull A) (Rhull B).
Variables (d : unit) (T : orderType d).
Implicit Types (a : itv_bound T) (x y : T) (i j : interval T) (b : bool).
Lemma setCitvl a : ~` [set` Interval -oo%O a] = [set` Interval a +oo%O].
Lemma setCitvr a : ~` [set` Interval a +oo%O] = [set` Interval -oo%O a].
Lemma set_itv_splitI i : [set` i] = [set` Interval i.1 +oo%O] `&` [set` Interval -oo%O i.2].
Lemma setCitv i :
~` [set` i] = [set` Interval -oo%O i.1] `|` [set` Interval i.2 +oo%O].
Lemma set_itv_splitD i :
[set` i] = [set` Interval i.1 +oo%O] `\` [set` Interval i.2 +oo%O].
End set_itv_porderType.
Section set_itv_realType.
Variable R : realType.
Implicit Types x : R.
Lemma set_itvK : {in neitv, cancel pred_set (@Rhull R)}.
Lemma RhullT : Rhull setT = `]-oo, +oo[%R :> interval R.
Lemma RhullK : {in (@is_interval _ : set (set R)), cancel (@Rhull R) pred_set}.
Lemma itv_c_inftyEbigcap x :
`[x, +oo[%classic = \bigcap_k `]x - k.+1%:R^-1, +oo[%classic.
Lemma itv_bnd_inftyEbigcup b x : [set` Interval (BSide b x) +oo%O] =
\bigcup_k [set` Interval (BSide b x) (BLeft k%:R)].
Lemma itv_o_inftyEbigcup x :
`]x, +oo[%classic = \bigcup_k `[x + k.+1%:R^-1, +oo[%classic.
Lemma set_itv_setT (i : interval R) : [set` i] = setT → i = `]-oo, +oo[.
End set_itv_realType.
Lemma set_itv_ge [disp : unit] [T : porderType disp] [b1 b2 : itv_bound T] :
~~ (b1 < b2)%O → [set` Interval b1 b2] = set0.
Section conv_factor_numDomainType.
Variable R : numDomainType.
Implicit Types (a b t r : R) (A : set R).
Lemma mem_1B_itvcc t : (1 - t \in `[0, 1]) = (t \in `[0, 1]).
Definition conv a b t : R := (1 - t) × a + t × b.
Lemma conv_id : conv 0 1 = id.
Lemma convEl a b t : conv a b t = t × (b - a) + a.
Lemma convEr a b t : conv a b t = (1 - t) × (a - b) + b.
Lemma conv10 t : conv 1 0 t = 1 - t.
Lemma conv0 a b : conv a b 0 = a.
Lemma conv1 a b : conv a b 1 = b.
Lemma conv_sym a b t : conv a b t = conv b a (1 - t).
Lemma conv_flat a : conv a a = cst a.
Lemma leW_conv a b : a ≤ b → {homo conv a b : x y / x ≤ y}.
Definition factor a b x := (x - a) / (b - a).
Lemma leW_factor a b : a ≤ b → {homo factor a b : x y / x ≤ y}.
Lemma factor_flat a : factor a a = cst 0.
Lemma factorl a b : factor a b a = 0.
Definition ndconv a b of a < b := conv a b.
Lemma ndconvE a b (ab : a < b) : ndconv ab = conv a b.
End conv_factor_numDomainType.
Section conv_factor_numFieldType.
Variable R : numFieldType.
Implicit Types (a b t r : R) (A : set R).
Lemma factorr a b : a != b → factor a b b = 1.
Lemma factorK a b : a != b → cancel (factor a b) (conv a b).
Lemma convK a b : a != b → cancel (conv a b) (factor a b).
Lemma conv_inj a b : a != b → injective (conv a b).
Lemma factor_inj a b : a != b → injective (factor a b).
Lemma conv_bij a b : a != b → bijective (conv a b).
Lemma factor_bij a b : a != b → bijective (factor a b).
Lemma le_conv a b : a < b → {mono conv a b : x y / x ≤ y}.
Lemma le_factor a b : a < b → {mono factor a b : x y / x ≤ y}.
Lemma lt_conv a b : a < b → {mono conv a b : x y / x < y}.
Lemma lt_factor a b : a < b → {mono factor a b : x y / x < y}.
Let ltNeq a b : a < b → a != b.
Lemma conv_itv_bij ba bb a b : a < b →
set_bij [set` Interval (BSide ba 0) (BSide bb 1)]
[set` Interval (BSide ba a) (BSide bb b)] (conv a b).
Lemma factor_itv_bij ba bb a b : a < b →
set_bij [set` Interval (BSide ba a) (BSide bb b)]
[set` Interval (BSide ba 0) (BSide bb 1)] (factor a b).
Lemma mem_conv_itv ba bb a b : a < b →
set_fun [set` Interval (BSide ba 0) (BSide bb 1)]
[set` Interval (BSide ba a) (BSide bb b)] (conv a b).
Lemma mem_conv_itvcc a b : a ≤ b → set_fun `[0, 1] `[a, b] (conv a b).
Lemma range_conv ba bb a b : a < b →
conv a b @` [set` Interval (BSide ba 0) (BSide bb 1)] =
[set` Interval (BSide ba a) (BSide bb b)].
Lemma range_factor ba bb a b : a < b →
factor a b @` [set` Interval (BSide ba a) (BSide bb b)] =
[set` Interval (BSide ba 0) (BSide bb 1)].
End conv_factor_numFieldType.
Lemma mem_factor_itv (R : realFieldType) ba bb (a b : R) :
set_fun [set` Interval (BSide ba a) (BSide bb b)]
[set` Interval (BSide ba 0) (BSide bb 1)] (factor a b).
Section Rhull_lemmas.
Variable R : realType.
Implicit Types (a b t r : R) (A : set R).
Lemma Rhull_smallest A : [set` Rhull A] = smallest (@is_interval R) A.
Lemma le_Rhull : {homo (@Rhull R) : A B / (A `<=` B) >-> {subset A ≤ B}}.
Lemma neitv_Rhull A : ~~ neitv (Rhull A) → A = set0.
Lemma Rhull_involutive A : Rhull [set` Rhull A] = Rhull A.
End Rhull_lemmas.
Coercion ereal_of_itv_bound T (b : itv_bound T) : \bar T :=
match b with BSide _ y ⇒ y%:E | +oo%O ⇒ +oo%E | -oo%O ⇒ -oo%E end.
Arguments ereal_of_itv_bound T !b.
Lemma le_bnd_ereal (R : realDomainType) (a b : itv_bound R) :
(a ≤ b)%O → (a ≤ b)%E.
Lemma lt_ereal_bnd (R : realDomainType) (a b : itv_bound R) :
(a < b)%E → (a < b)%O.
Lemma neitv_bnd1 (R : numFieldType) (s : seq (interval R)) :
all neitv s → ∀ i, i \in s → i.1 != +oo%O.
Lemma neitv_bnd2 (R : numFieldType) (s : seq (interval R)) :
all neitv s → ∀ i, i \in s → i.2 != -oo%O.
Lemma Interval_ereal_mem (R : realDomainType) (r : R) (a b : itv_bound R) :
r \in Interval a b → (a ≤ r%:E ≤ b)%E.
Lemma ereal_mem_Interval (R : realDomainType) (r : R) (a b : itv_bound R) :
(a < r%:E < b)%E → r \in Interval a b.
Lemma trivIset_set_itv_nth (R : numDomainType) def (s : seq (interval R))
(D : set nat) : [set` def] = set0 →
trivIset D (fun i ⇒ [set` nth def s i]) ↔
trivIset D (fun i ⇒ nth set0 [seq [set` j] | j <- s] i).
Arguments trivIset_set_itv_nth {R} _ {s}.
Section disjoint_itv.
Context {R : numDomainType}.
Definition disjoint_itv : rel (interval R) :=
fun a b ⇒ [disjoint [set` a] & [set` b]].
Lemma disjoint_itvxx (i : interval R) : neitv i → ~~ disjoint_itv i i.
Lemma lt_disjoint (i j : interval R) :
(∀ x y, x \in i → y \in j → x < y) → disjoint_itv i j.
End disjoint_itv.
Lemma disjoint_neitv {R : realFieldType} (i j : interval R) :
disjoint_itv i j ↔ ~~ neitv (itv_meet i j).
Lemma disj_itv_Rhull {R : realType} (A B : set R) : A `&` B = set0 →
is_interval A → is_interval B → disjoint_itv (Rhull A) (Rhull B).