Library mathcomp.classical.set_interval
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From mathcomp Require Import all_ssreflect ssralg ssrnum interval.
From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
From HB Require Import structures.
From mathcomp.classical Require Import functions.
From mathcomp Require Import all_ssreflect ssralg ssrnum interval.
From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
From HB Require Import structures.
From mathcomp.classical Require Import functions.
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
line_path a b t := (1 - t) * a + t * b, convexity operator over a
numDomainType
ndline_path == line_path a b with the constraint that a < b
factor a b x := (x - a) / (b - a)
set_itvE == multirule to turn intervals into inequalities
disjoint_itv i j == intervals i and j are disjoint
Set Implicit Arguments.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
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 in1_subset_itv (P : T → Prop) i j :
[set` j] `<=` [set` i] → {in i, ∀ x, P x} → {in j, ∀ x, P x}.
Lemma subset_itvW x y z u b0 b1 :
(x ≤ y)%O → (z ≤ u)%O →
`]y, z[ `<=` [set` Interval (BSide b0 x) (BSide b1 u)].
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} _.
Lemma set_itv_ge [disp : unit] [T : porderType disp] [b1 b2 : itv_bound T] :
~~ (b1 < b2)%O → [set` Interval b1 b2] = set0.
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 subr_image.
Variable R : numDomainType.
Implicit Types E : set R.
Implicit Types x : R.
Lemma setNK : involutive (fun E ⇒ -%R @` E).
Lemma lb_ubN E x : lbound E x ↔ ubound (-%R @` E) (- x).
Lemma ub_lbN E x : ubound E x ↔ lbound (-%R @` E) (- x).
Lemma memNE E x : E x = (-%R @` E) (- x).
Lemma nonemptyN E : nonempty (-%R @` E) ↔ nonempty E.
Lemma opp_set_eq0 E : (-%R @` E) = set0 ↔ E = set0.
Lemma has_lb_ubN E : has_lbound E ↔ has_ubound (-%R @` E).
End subr_image.
Section interval_hasNbound.
Variable R : realDomainType.
Implicit Types E : set R.
Implicit Types x : R.
Lemma has_ubPn {E} : ¬ has_ubound E ↔ (∀ x, exists2 y, E y & x < y).
Lemma has_lbPn E : ¬ has_lbound E ↔ (∀ x, exists2 y, E y & y < x).
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.
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))].
Lemma opp_itvoo (R : numDomainType) (x y : R) :
-%R @` `]x, y[%classic = `](- y), (- x)[%classic.
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 in1_subset_itv (P : T → Prop) i j :
[set` j] `<=` [set` i] → {in i, ∀ x, P x} → {in j, ∀ x, P x}.
Lemma subset_itvW x y z u b0 b1 :
(x ≤ y)%O → (z ≤ u)%O →
`]y, z[ `<=` [set` Interval (BSide b0 x) (BSide b1 u)].
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} _.
Lemma set_itv_ge [disp : unit] [T : porderType disp] [b1 b2 : itv_bound T] :
~~ (b1 < b2)%O → [set` Interval b1 b2] = set0.
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 subr_image.
Variable R : numDomainType.
Implicit Types E : set R.
Implicit Types x : R.
Lemma setNK : involutive (fun E ⇒ -%R @` E).
Lemma lb_ubN E x : lbound E x ↔ ubound (-%R @` E) (- x).
Lemma ub_lbN E x : ubound E x ↔ lbound (-%R @` E) (- x).
Lemma memNE E x : E x = (-%R @` E) (- x).
Lemma nonemptyN E : nonempty (-%R @` E) ↔ nonempty E.
Lemma opp_set_eq0 E : (-%R @` E) = set0 ↔ E = set0.
Lemma has_lb_ubN E : has_lbound E ↔ has_ubound (-%R @` E).
End subr_image.
Section interval_hasNbound.
Variable R : realDomainType.
Implicit Types E : set R.
Implicit Types x : R.
Lemma has_ubPn {E} : ¬ has_ubound E ↔ (∀ x, exists2 y, E y & x < y).
Lemma has_lbPn E : ¬ has_lbound E ↔ (∀ x, exists2 y, E y & y < x).
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.
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))].
Lemma opp_itvoo (R : numDomainType) (x y : R) :
-%R @` `]x, y[%classic = `](- y), (- x)[%classic.
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 line_path_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 line_path a b t : R := (1 - t) × a + t × b.
Lemma line_path_id : line_path 0 1 = id.
Lemma line_pathEl a b t : line_path a b t = t × (b - a) + a.
Lemma line_pathEr a b t : line_path a b t = (1 - t) × (a - b) + b.
Lemma line_path10 t : line_path 1 0 t = 1 - t.
Lemma line_path0 a b : line_path a b 0 = a.
Lemma line_path1 a b : line_path a b 1 = b.
Lemma line_path_sym a b t : line_path a b t = line_path b a (1 - t).
Lemma line_path_flat a : line_path a a = cst a.
Lemma leW_line_path a b : a ≤ b → {homo line_path 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 ndline_path a b of a < b := line_path a b.
Lemma ndline_pathE a b (ab : a < b) : ndline_path ab = line_path a b.
End line_path_factor_numDomainType.
Section line_path_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) (line_path a b).
Lemma line_pathK a b : a != b → cancel (line_path a b) (factor a b).
Lemma line_path_inj a b : a != b → injective (line_path a b).
Lemma factor_inj a b : a != b → injective (factor a b).
Lemma line_path_bij a b : a != b → bijective (line_path a b).
Lemma factor_bij a b : a != b → bijective (factor a b).
Lemma le_line_path a b : a < b → {mono line_path a b : x y / x ≤ y}.
Lemma le_factor a b : a < b → {mono factor a b : x y / x ≤ y}.
Lemma lt_line_path a b : a < b → {mono line_path 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 line_path_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)] (line_path 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_line_path_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)] (line_path a b).
Lemma mem_line_path_itvcc a b : a ≤ b → set_fun `[0, 1] `[a, b] (line_path a b).
Lemma range_line_path ba bb a b : a < b →
line_path 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)].
Lemma onem_factor a b x : a != b → `1-(factor a b x) = factor b a x.
End line_path_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).
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 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).
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 line_path_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 line_path a b t : R := (1 - t) × a + t × b.
Lemma line_path_id : line_path 0 1 = id.
Lemma line_pathEl a b t : line_path a b t = t × (b - a) + a.
Lemma line_pathEr a b t : line_path a b t = (1 - t) × (a - b) + b.
Lemma line_path10 t : line_path 1 0 t = 1 - t.
Lemma line_path0 a b : line_path a b 0 = a.
Lemma line_path1 a b : line_path a b 1 = b.
Lemma line_path_sym a b t : line_path a b t = line_path b a (1 - t).
Lemma line_path_flat a : line_path a a = cst a.
Lemma leW_line_path a b : a ≤ b → {homo line_path 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 ndline_path a b of a < b := line_path a b.
Lemma ndline_pathE a b (ab : a < b) : ndline_path ab = line_path a b.
End line_path_factor_numDomainType.
Section line_path_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) (line_path a b).
Lemma line_pathK a b : a != b → cancel (line_path a b) (factor a b).
Lemma line_path_inj a b : a != b → injective (line_path a b).
Lemma factor_inj a b : a != b → injective (factor a b).
Lemma line_path_bij a b : a != b → bijective (line_path a b).
Lemma factor_bij a b : a != b → bijective (factor a b).
Lemma le_line_path a b : a < b → {mono line_path a b : x y / x ≤ y}.
Lemma le_factor a b : a < b → {mono factor a b : x y / x ≤ y}.
Lemma lt_line_path a b : a < b → {mono line_path 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 line_path_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)] (line_path 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_line_path_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)] (line_path a b).
Lemma mem_line_path_itvcc a b : a ≤ b → set_fun `[0, 1] `[a, b] (line_path a b).
Lemma range_line_path ba bb a b : a < b →
line_path 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)].
Lemma onem_factor a b x : a != b → `1-(factor a b x) = factor b a x.
End line_path_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).
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 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).