Top source

Module mathcomp.classical.set_interval

From HB Require Import structures.
From mathcomp Require Import boot order ssralg ssrnum interval.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import boolp classical_sets functions.


Unset SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Section set_itv_porderType.
Context {

disp

---

Source code

} {

T

---

Source code

: porderType disp}.
Implicit Types (i j : interval T) (x y : T) (a : itv_bound T).

Definition

neitv

continuous_at : forall [T U : nbhsType], T -> (T -> U) -> Prop continuous_at is not universe polymorphic Arguments continuous_at [T U] x f%_function_scope continuous_at is transparent Expands to: Constant mathcomp.classical.filter.continuous_at Declared in library mathcomp.classical.filter, line 973, characters 11-24

---

Source code

i

---

Source code

:= [set` i] != set0.

Lemma

neitv_lt_bnd

---

Source code

i

---

Source code

: neitv i -> (i.1 < i.2)%O.

Proof.

case: i => a b; apply: contraNT => /= /itv_ge ab0.
by apply/eqP; rewrite predeqE => t; split => //=; rewrite ab0.
Qed.

Lemma

set_itvP

---

Source code

i

---

Source code

j

---

Source code

: [set` i] = [set` j] :> set _ <-> i =i j.

Proof.

split => [ij x|ij]; first by have /(congr1 (@^~ x))/=/is_true_inj := ij.
by rewrite predeqE => r /=; rewrite ij.
Qed.

Lemma

subset_itvP

---

Source code

i

---

Source code

j

---

Source code

: {subset i <= j} <-> [set` i] `<=` [set` j].

Proof.

by []. Qed.

Lemma

in1_subset_itv

---

Source code

(

P

---

Source code

: T -> Prop)

i

---

Source code

j

---

Source code

:
  [set` j] `<=` [set` i] -> {in i, forall

x

---

Source code

, P x} -> {in j, forall

x

---

Source code

, P x}.

Proof.

by move=> /subset_itvP ji iP z zB; apply: iP; exact: ji. Qed.

Lemma

subset_itvW

---

Source code

x

---

Source code

y

---

Source code

z

---

Source code

u

---

Source code

b0

---

Source code

b1

---

Source code

:
    (x <= y)%O -> (z <= u)%O ->
  `]y, z[ `<=` [set` Interval (BSide b0 x) (BSide b1 u)].

Proof.

move=> xy zu; apply: (@subset_trans _ `]x, u[%classic).
  move=> x0/=; rewrite 2!in_itv/= => /andP[].
  by move=> /(le_lt_trans xy) ->/= /lt_le_trans; exact.
by move: b0 b1 => [] [] /=; [exact: subset_itv_oo_co|exact: subset_itv_oo_cc|
  exact: subset_refl|exact: subset_itv_oo_oc].
Qed.

Lemma

subset_itvl

---

Source code

(

a

---

Source code

b

---

Source code

c

---

Source code

: itv_bound T) : (b <= c)%O ->
  [set` Interval a b] `<=` [set` Interval a c].

Proof.

by move=> /subitvPr /subsetP h; apply/subsetP => x /h. Qed.

Lemma

subset_itvr

---

Source code

(

a

---

Source code

b

---

Source code

c

---

Source code

: itv_bound T) : (c <= a)%O ->
  [set` Interval a b] `<=` [set` Interval c b].

Proof.

by move=> /subitvPl /subsetP h; apply/subsetP => x /h. Qed.

Lemma

subset_itv

---

Source code

(

a

---

Source code

b

---

Source code

c

---

Source code

d

---

Source code

: itv_bound T) : (c <= a)%O -> (b <= d)%O ->
  [set` Interval a b] `<=` [set` Interval c d].

Proof.

by move=> ac bd; apply/(subset_trans (subset_itvl _))/subset_itvr. Qed.

Lemma

subset_itvScc

---

Source code

(

a

---

Source code

b

---

Source code

: itv_bound T) (

c

---

Source code

e

---

Source code

: T) :
    (BLeft c <= a)%O -> (b <= BRight e)%O ->
  [set` Interval a b] `<=` [set` `[c, e]].

Proof.

move=> ca be z/=; rewrite !in_itv/==> /andP[az zb].
case: a ca az => [[|]/=|[|]//] a; rewrite bnd_simp => ca az.
- rewrite (le_trans ca az)/=.
  move: b be zb => [[|]/= b|[|]//]; rewrite bnd_simp => be.
    by move=> /ltW/le_trans; exact.
  by move=> /le_trans; exact.
- rewrite (le_trans ca (ltW az))/=.
  move: b be zb => [[|]/= b|[|]//]; rewrite bnd_simp => be.
    by move=> /ltW/le_trans; exact.
  by move=> /le_trans; exact.
Qed.

Lemma

subset_itvSoo

---

Source code

(

a

---

Source code

b

---

Source code

: itv_bound T) (

c

---

Source code

e

---

Source code

: T) :
    (BLeft c < a)%O -> (b < BRight e)%O ->
  [set` Interval a b] `<=` [set` `]c, e[].

Proof.

move=> ca be z/=; rewrite !in_itv/= => /andP[az zb].
case: a ca az => [[|]/=|[|]//] a; rewrite bnd_simp => ca az.
  rewrite (lt_le_trans ca az)/=.
  move: b be zb => [[|]/= b|[|]//]; rewrite bnd_simp => be.
    by move=> /lt_le_trans; exact.
  by move=> /le_lt_trans; exact.
rewrite (le_lt_trans ca az)/=.
move: b be zb => [[|]/= b|[|]//]; rewrite bnd_simp => be.
  by move=> /lt_le_trans; exact.
by move=> /le_lt_trans; exact.
Qed.

Lemma

set_itvoo

---

Source code

x

---

Source code

y

---

Source code

: `]x, y[%classic = [set

z

---

Source code

| (x < z < y)%O].

Proof.

by []. Qed.

Lemma

set_itvco

---

Source code

x

---

Source code

y

---

Source code

: `[x, y[%classic = [set

z

---

Source code

| (x <= z < y)%O].

Proof.

by []. Qed.

Lemma

set_itvcc

---

Source code

x

---

Source code

y

---

Source code

: `[x, y]%classic = [set

z

---

Source code

| (x <= z <= y)%O].

Proof.

by []. Qed.

Lemma

set_itvoc

---

Source code

x

---

Source code

y

---

Source code

: `]x, y]%classic = [set

z

---

Source code

| (x < z <= y)%O].

Proof.

by []. Qed.

Lemma

set_itv1

---

Source code

x

---

Source code

: `[x, x]%classic = [set x].

Proof.

by apply/seteqP; split=> y /=; rewrite itvxx ?inE (rwP eqP). Qed.

Lemma

set_itvoo0

---

Source code

x

---

Source code

: `]x, x[%classic = set0.

Proof.

by rewrite -subset0 => y /=; rewrite itv_ge//= bnd_simp ltxx. Qed.

Lemma

set_itvoc0

---

Source code

x

---

Source code

: `]x, x]%classic = set0.

Proof.

by rewrite -subset0 => y /=; rewrite itv_ge//= bnd_simp ltxx. Qed.

Lemma

set_itvco0

---

Source code

x

---

Source code

: `[x, x[%classic = set0.

Proof.

by rewrite -subset0 => y /=; rewrite itv_ge//= bnd_simp ltxx. Qed.

Lemma

set_itvNyy

---

Source code

: `]-oo, +oo[%classic = @setT T.

Proof.

by rewrite predeqE. Qed.

Lemma

set_itvoy

---

Source code

x

---

Source code

: `]x, +oo[%classic = [set

z

---

Source code

| (x < z)%O].

Proof.

by rewrite predeqE => r /=; rewrite in_itv andbT. Qed.

Lemma

set_itvcy

---

Source code

x

---

Source code

: `[x, +oo[%classic = [set

z

---

Source code

| (x <= z)%O].

Proof.

by rewrite predeqE /mkset => r; rewrite in_itv andbT. Qed.

Lemma

set_itvNyo

---

Source code

x

---

Source code

: `]-oo, x[%classic = [set

z

---

Source code

| (z < x)%O].

Proof.

by rewrite predeqE /mkset => r; rewrite in_itv. Qed.

Lemma

set_itvNyc

---

Source code

x

---

Source code

: `]-oo, x]%classic = [set

z

---

Source code

| (z <= x)%O].

Proof.

by rewrite predeqE /mkset => r; rewrite in_itv. Qed.

Lemma

set_itv_ybnd

---

Source code

a

---

Source code

: [set` Interval +oo%O a] = set0.

Proof.

by apply/eqP/negPn/negP => /neitv_lt_bnd. Qed.

Lemma

set_itv_bndNy

---

Source code

a

---

Source code

: [set` Interval a -oo%O] = set0.

Proof.

by apply/eqP/negPn/negP => /neitv_lt_bnd /=; case: a => [[]a|[]]. Qed.

Definition

set_itv_infty_set0

globally : forall {T : Type}, set T -> set_system T globally is not universe polymorphic Arguments globally {T}%_type_scope A%_classical_set_scope _ / The reduction tactics unfold globally when applied to 3 arguments globally is transparent Expands to: Constant mathcomp.classical.filter.globally Declared in library mathcomp.classical.filter, line 999, characters 11-19

---

Source code

:= (set_itv_bndNy, set_itv_ybnd).

Definition

set_itvE

frechet_filter : forall [T : Type], set (set T) frechet_filter is not universe polymorphic Arguments frechet_filter [T]%_type_scope _ frechet_filter is transparent Expands to: Constant mathcomp.classical.filter.frechet_filter Declared in library mathcomp.classical.filter, line 1021, characters 11-25

---

Source code

:= (set_itv1, set_itvoo0, set_itvoc0, set_itvco0, set_itvoo,
  set_itvcc, set_itvoc, set_itvco, set_itvNyy, set_itvoy,
  set_itvcy, set_itvNyo, set_itvNyc, set_itv_infty_set0).

Lemma

set_itvxx

---

Source code

a

---

Source code

: [set` Interval a a] = set0.

Proof.

by move: a => [[|] a |[|]]; rewrite !set_itvE. Qed.

Lemma

setU_itvob1

---

Source code

a

---

Source code

x

---

Source code

: (a <= BLeft x)%O ->
  [set` Interval a (BLeft x)] `|` [set x] = [set` Interval a (BRight x)].

Proof.

move=> ax; apply/predeqP => z /=; rewrite itv_splitU1// [in X in _ <-> X]inE.
by rewrite (rwP eqP) (rwP orP) orbC.
Qed.

Lemma

setU_1itvob

---

Source code

a

---

Source code

x

---

Source code

: (BRight x <= a)%O ->
  x |` [set` Interval (BRight x) a] = [set` Interval (BLeft x) a].

Proof.

move=> ax; apply/predeqP => z /=; rewrite itv_split1U// [in X in _ <-> X]inE.
by rewrite (rwP eqP) (rwP orP) orbC.
Qed.

Lemma

setUitv1

---

Source code

a

---

Source code

x

---

Source code

b

---

Source code

: (a <= BLeft x)%O ->
  [set` Interval a (BSide b x)] `|` [set x] = [set` Interval a (BRight x)].

Proof.

move=> ax; case: b; [exact: setU_itvob1|].
by apply: setUidl => ? /= ->; rewrite itv_boundlr ax lexx.
Qed.

Lemma

setU1itv

---

Source code

a

---

Source code

x

---

Source code

b

---

Source code

: (BRight x <= a)%O ->
  x |` [set` Interval (BSide b x) a] = [set` Interval (BLeft x) a].

Proof.

move=> ax; case: b; [|exact: setU_1itvob].
by apply: setUidr => ? /= ->; rewrite itv_boundlr ax lexx.
Qed.

Lemma

setUitv_set2

---

Source code

x

---

Source code

y

---

Source code

b1

---

Source code

b2

---

Source code

:
  (x <= y)%O ->
  [set` Interval (BSide b1 x) (BSide b2 y)] `|` [set x; y] = `[x, y]%classic.

Proof.

rewrite le_eqVlt => /orP [/eqP->|xy].
  by case: b1; case: b2; rewrite !set_itvE !setUid // set0U.
rewrite setUCA setUitv1; first by case: b1; rewrite bnd_simp// ltW.
by rewrite setU1itv// bnd_simp ltW.
Qed.

Lemma

setDitv1r

---

Source code

a

---

Source code

x

---

Source code

b

---

Source code

:
  [set` Interval a (BSide b x)] `\ x = [set` Interval a (BLeft x)].

Proof.

case: b; first by apply: not_setD1; rewrite /= in_itv/= ltxx andbF.
apply/seteqP; split => [z|z] /=; rewrite !in_itv/=.
  by move=> [/andP[-> /= zx] /eqP xz]; rewrite lt_neqAle xz.
by rewrite lt_neqAle => /andP[-> /andP[/eqP ? ->]].
Qed.

Lemma

setDitv1l

---

Source code

a

---

Source code

x

---

Source code

b

---

Source code

:
  [set` Interval (BSide b x) a] `\ x = [set` Interval (BRight x) a].

Proof.

case: b; last by apply: not_setD1; rewrite /= in_itv/= ltxx.
apply/seteqP; split => [z|z] /=; rewrite !in_itv/=.
  move=> [/andP[xz ->]]; rewrite andbT => /eqP.
  by rewrite lt_neqAle eq_sym => ->.
move=> /andP[]; rewrite lt_neqAle => /andP[xz zx ->].
by rewrite andbT; split => //; exact/nesym/eqP.
Qed.

Lemma

setDitv_set2

---

Source code

x

---

Source code

y

---

Source code

b1

---

Source code

b2

---

Source code

:
  [set` Interval (BSide b1 x) (BSide b2 y)] `\` [set x; y] = `]x, y[%classic.

Proof.

by rewrite -setDDl setDitv1l setDitv1r. Qed.

End set_itv_porderType.
Arguments neitv {disp T} _.
#[deprecated(since="mathcomp-analysis 1.15.0", note="use `set_itv1` instead")]
Notation

interval_set1

---

Source code

:= set_itv1 (only parsing).

Section set_itv_orderType.
Context {

d

---

Source code

} {

T

---

Source code

: orderType d}.
Implicit Types a b x y : itv_bound T.

Lemma

itv_bndbnd_setU

---

Source code

a

---

Source code

x

---

Source code

y

---

Source code

: (a <= x)%O -> (x <= y)%O ->
  ([set` Interval a y] = [set` Interval a x] `|` [set` Interval x y])%classic.

Proof.

rewrite le_eqVlt => /predU1P[<-{x} ay|]; first by rewrite set_itvxx set0U.
move=> /[swap].
rewrite le_eqVlt => /predU1P[-> ay|]; first by rewrite set_itvxx setU0.
move: y => [yb y/=|[|]]; last 2 first.
  by case: x => [|[|]].
  move=> _ ax; apply/seteqP; split => [z|z] /=.
    rewrite !in_itv/= !andbT => -> /=; apply/orP.
    by move: x => [[|] x/=|[|]//] in ax *; rewrite leNgt ?(orbN,orNb).
  rewrite !in_itv/= !andbT => -[/andP[]|]//.
  move: x => [[|] x/=|[|]//] in ax *; move: a => [[|] a/=|[|]//] in ax * => //.
  - by apply/le_trans; exact/ltW.
  - exact/lt_le_trans.
  - by move=> /(le_lt_trans ax) /ltW.
  - exact/lt_trans.
move=> xy ax; apply/seteqP; split => [z|z] /=.
  rewrite !in_itv /= => /andP[].
  move: a ax => [b t /=|[]//= oox _].
    move=> tx -> zxy /=; rewrite zxy andbT/=; apply/orP.
    by case: x xy tx => [[|] x/=|[|]//] xy tx; rewrite leNgt ?(orbN,orNb).
  move=> ->; rewrite andbT; apply/orP.
  by move: x => [[|] x/=|[|]//] in oox xy *; rewrite leNgt ?(orbN,orNb).
rewrite !in_itv/=.
move: a ax => [b t /= tx| [/= oox|/= oox]].
- move=> [/andP[-> zx]|].
    move: x => [[|] x|[|]//]/= in xy tx zx *.
      case: yb => /= in xy *.
        by rewrite (lt_trans zx _).
      by rewrite (ltW (lt_le_trans zx _)).
    rewrite bnd_simp in xy.
    case: yb => /=.
      by rewrite (le_lt_trans zx _).
    by rewrite (ltW (le_lt_trans zx _)).
  move: x => [[|] x|[|]//]/= in xy tx *; rewrite bnd_simp in xy tx.
  + move=> /andP[xz ->]; rewrite andbT.
    case: b => /=.
      by rewrite (le_trans _ xz)// ltW.
    by rewrite (lt_le_trans tx).
  move=> /andP[xz ->]; rewrite andbT.
  case: b tx => /= tx; rewrite bnd_simp in tx.
    by rewrite ltW// (le_lt_trans _ xz).
  by rewrite (lt_trans tx).
- move: x => [[|] x|[|]//]/= in xy oox *; move=> [|].
  + case: yb => /= in xy *.
      by move=> /lt_trans; exact.
    rewrite bnd_simp in xy.
    by move=> /lt_le_trans => /(_ _ xy)/ltW.
  + by move=> /andP[].
  + case: yb => /= in xy *.
      by move=> /le_lt_trans; apply.
    by move=> /le_trans; apply; exact/ltW.
  + by move=> /andP[].
- by move: x => [[|] x|[|]//]/= in xy oox *.
Qed.

Lemma

set_itv_splitU

---

Source code

a

---

Source code

b

---

Source code

(

c

---

Source code

: T) : c \in Interval a b ->
  [set` Interval a b] `\ c =
    [set` Interval a (BLeft c)] `|` [set` Interval (BRight c) b].

Proof.

move=> cab; apply/seteqP; split => [x /= [xab /eqP]|x[|]]/=.
- rewrite neq_lt => /orP[xc|cx]; [left|right].
  + move: cab xab; rewrite !itv_boundlr => /andP[ac cb] /andP[ax xb].
    by rewrite ax/= bnd_simp.
  + move: cab xab; rewrite !itv_boundlr => /andP[ac cb] /andP[ax xb].
    by rewrite xb andbT bnd_simp.
- move: cab; rewrite !itv_boundlr => /andP[ac cb] /andP[ax].
  rewrite bnd_simp => xc.
  rewrite ax/= (le_trans _ cb) ?bnd_simp ?(ltW xc)//; split => //.
  by apply/eqP; rewrite lt_eqF.
- move: cab; rewrite !itv_boundlr => /andP[ac cb] /andP[+ xb].
  rewrite bnd_simp => cx.
  rewrite xb/= andbT (le_trans ac)/= ?bnd_simp ?(ltW cx)//; split => //.
  by apply/eqP; rewrite gt_eqF.
Qed.

Lemma

setDitvoo

---

Source code

(

x

---

Source code

y

---

Source code

: T) (

b1

---

Source code

b2

---

Source code

: bool) :
  neitv (Interval (BSide b1 x) (BSide b2 y)) ->
  [set` Interval (BSide b1 x) (BSide b2 y)] `\` `]x, y[ =
  (if b1 then [set x] else set0) `|` (if b2 then set0 else [set y]).

Proof.

move=> /neitv_lt_bnd/= xy.
apply/seteqP; split => z/=; rewrite !in_itv/=; last first.
  move: b1 b2 xy.
  by move=> [] [] /[!bnd_simp]/= + []// -> => ->; rewrite ?(lexx,ltxx,andbF).
case=> /[swap] /negP; rewrite negb_and.
move: b1 b2 {xy} => [] [] /= + /andP[]; rewrite ?ltNge !negbK.
- by move=> /orP[*|->//]; left; exact/le_anti/andP.
- by case/orP => *; [left|right]; exact/le_anti/andP.
- by case/orP => ->.
- by move=> /orP[->//|*]; right; exact/le_anti/andP.
Qed.

Lemma

setDccitv

---

Source code

(

x

---

Source code

y

---

Source code

: T) (

b1

---

Source code

b2

---

Source code

: bool) :
  neitv `[x, y] ->
  `[x, y] `\` [set` Interval (BSide b1 x) (BSide b2 y)] =
  (if b1 then set0 else [set x]) `|` (if b2 then [set y] else set0).

Proof.

move=> /neitv_lt_bnd/= xy.
apply/seteqP; split => z/=; rewrite !in_itv/=; last first.
  move: b1 b2 xy.
  by move=> [] [] /[!bnd_simp]/= + []// -> => ->; rewrite ?(lexx,ltxx,andbF).
case=> /[swap] /negP; rewrite negb_and.
move: b1 b2 {xy} => [] [] /= + /andP[]; rewrite -?leNgt.
- by move=> /orP[/negPf ->//|*]; right; exact/le_anti/andP.
- by case/orP => /negPf ->.
- by case/orP => *; [left|right]; exact/le_anti/andP.
- by move=> /orP[*|/negPf ->//]; left; exact/le_anti/andP.
Qed.

Lemma

setDitvoy

---

Source code

a

---

Source code

(

x

---

Source code

: T) (

b

---

Source code

: bool) :
  neitv (Interval (BSide b x) a) ->
  [set` Interval (BSide b x) a] `\` `]x, +oo[ = if b then [set x] else set0.

Proof.

move/neitv_lt_bnd => /= bxa; apply/seteqP; split => z/=; rewrite !in_itv/=.
- case: b {bxa}; rewrite /= andbT; last by case=> /andP[->].
  by case=> /andP[? _] /negP; rewrite -leNgt => ?; exact/le_anti/andP.
- case: b bxa => //= /[swap] <-.
  by move: a => [[] ?|[]]; rewrite !bnd_simp.
Qed.

Lemma

setDitvNyo

---

Source code

a

---

Source code

(

x

---

Source code

: T) (

b

---

Source code

: bool) :
  neitv (Interval a (BSide b x)) ->
  [set` Interval a (BSide b x)] `\` `]-oo, x[ = if b then set0 else [set x].

Proof.

move/neitv_lt_bnd => /= abx; apply/seteqP; split => z/=; rewrite !in_itv/=.
- case: b {abx} => /=; first by case=> /andP[_ ->].
  by case=> /andP[_ ?] /negP; rewrite -leNgt => ?; exact/le_anti/andP.
- case: b abx => //= /[swap] <-.
  by move: a => [[] ?|[]]; rewrite !bnd_simp// andbT.
Qed.

Lemma

setD_cbnd_bndy

---

Source code

a

---

Source code

(

x

---

Source code

: T) (

b

---

Source code

: bool) :
  neitv (Interval (BLeft x) a) ->
  [set` Interval (BLeft x) a] `\` [set` Interval (BSide b x) +oo%O] =
  (if b then set0 else [set x]).

Proof.

move/neitv_lt_bnd => /= xa; apply/seteqP; split => z/=; rewrite !in_itv/=.
- case: b {xa}; rewrite /= andbT; first by case=> /andP[->].
  by case=> /andP[? _] /negP; rewrite -leNgt => ?; exact/le_anti/andP.
- case: b xa => //= /[swap] <-.
  by move: a => [[] ?|[]]; rewrite /= !bnd_simp.
Qed.

Lemma

setD_bndc_Nybnd

---

Source code

a

---

Source code

(

x

---

Source code

: T) (

b

---

Source code

: bool) :
  neitv (Interval a (BRight x)) ->
  [set` Interval a (BRight x)] `\` [set` Interval -oo%O (BSide b x)] =
  (if b then [set x] else set0).

Proof.

move/neitv_lt_bnd => /= ax; apply/seteqP; split => z/=; rewrite !in_itv/=.
- case: b {ax} => /=; last by case=> /andP[_ ->].
  by case=> /andP[_ ?] /negP; rewrite -leNgt => ?; exact/le_anti/andP.
- case: b ax => //= /[swap] <-.
  by move: a => [[] ?|[]]; rewrite /= !bnd_simp// andbT.
Qed.

End set_itv_orderType.

Lemma

set_itv_ge

---

Source code

disp

---

Source code

[

T

---

Source code

: porderType disp] [

b1

---

Source code

b2

---

Source code

: itv_bound T] :
  ~~ (b1 < b2)%O -> [set` Interval b1 b2] = set0.

Proof.

by move=> Nb12; rewrite -subset0 => x /=; rewrite itv_ge. Qed.

Section set_itv_latticeType.
Context {

d

---

Source code

} {

T

---

Source code

: latticeType d}.
Implicit Types (i j : interval T) (x y : T) (a : itv_bound T).

Lemma

set_itvI

---

Source code

i

---

Source code

j

---

Source code

: [set` (i `&` j)%O] = [set` i] `&` [set` j].

Proof.

by apply/seteqP; split=> x /=; rewrite in_itvI (rwP andP). Qed.

End set_itv_latticeType.

Section set_itv_numFieldType.
Context {

R

---

Source code

: numFieldType}.
Implicit Types i : interval R.

Lemma

neitvE

---

Source code

i

---

Source code

: neitv i = (i.1 < i.2)%O.

Proof.

apply/idP/idP; first exact: neitv_lt_bnd.
by move=> /mem_miditv ii; apply/set0P; exists (miditv i).
Qed.

Lemma

neitvP

---

Source code

i

---

Source code

: reflect (i.1 < i.2)%O (neitv i).

Proof.

by apply: (iffP idP); rewrite -neitvE. Qed.

End set_itv_numFieldType.

Lemma

setitv0

---

Source code

(

R

---

Source code

: realDomainType) : [set` (\bot%O : interval R)] = set0.

Proof.

by rewrite predeqE. Qed.

Section interval_has_bound.
Context {

R

---

Source code

: numDomainType}.

Lemma

has_lbound_itv

---

Source code

(

x

---

Source code

: R)

b

---

Source code

(

a

---

Source code

: itv_bound R) :
  has_lbound [set` Interval (BSide b x) a].

Proof.

by case: b; exists x => r /andP[]; rewrite bnd_simp // => /ltW. Qed.

Lemma

has_ubound_itv

---

Source code

(

x

---

Source code

: R)

b

---

Source code

(

a

---

Source code

: itv_bound R) :
  has_ubound [set` Interval a (BSide b x)].

Proof.

by case: b; exists x => r /andP[]; rewrite bnd_simp // => _ /ltW. Qed.

End interval_has_bound.

Section subr_image.
Context {

R

---

Source code

: numDomainType}.
Implicit Types (E : set R) (x : R).

Lemma

setNK

---

Source code

: involutive (fun

E

---

Source code

=> -%R @` E).

Proof.

move=> A; rewrite image_comp (_ : _ \o _ = id) ?image_id//.
by rewrite funeqE => r /=; rewrite opprK.
Qed.

Lemma

lb_ubN

---

Source code

E

---

Source code

x

---

Source code

: lbound E x <-> ubound (-%R @` E) (- x).

Proof.

split=> [/lbP xlbE|/ubP xlbE].
by move=> _ [z Ez <-]; rewrite lerNr opprK; apply xlbE.
by move=> y Ey; rewrite -(opprK x) lerNl; apply xlbE; exists y.
Qed.

Lemma

ub_lbN

---

Source code

E

---

Source code

x

---

Source code

: ubound E x <-> lbound (-%R @` E) (- x).

Proof.

split=> [? | /lb_ubN]; first by apply/lb_ubN; rewrite opprK setNK.
by rewrite opprK setNK.
Qed.

Lemma

memNE

---

Source code

E

---

Source code

x

---

Source code

: E x = (-%R @` E) (- x).

Proof.

by rewrite image_inj //; exact: oppr_inj. Qed.

Lemma

nonemptyN

---

Source code

E

---

Source code

: nonempty (-%R @` E) <-> nonempty E.

Proof.

split=> [[x ENx]|[x Ex]]; exists (- x); last by rewrite -memNE.
by rewrite memNE opprK.
Qed.

Lemma

opp_set_eq0

---

Source code

E

---

Source code

: (-%R @` E) = set0 <-> E = set0.

Proof.

by split; apply: contraPP => /eqP/set0P/nonemptyN/set0P/eqP. Qed.

Lemma

has_lb_ubN

---

Source code

E

---

Source code

: has_lbound E <-> has_ubound (-%R @` E).

Proof.

by split=> [[x /lb_ubN] | [x /ub_lbN]]; [|rewrite setNK]; exists (- x).
Qed.

End subr_image.

Section interval_hasNbound.
Context {

R

---

Source code

: realDomainType}.
Implicit Types (E : set R) (x : R).

Lemma

has_ubPn

---

Source code

{

E

---

Source code

} : ~ has_ubound E <-> (forall

x

---

Source code

, exists2

y

---

Source code

, E y & x < y).

Proof.

split; last first.
  move=> h [x] /ubP hle; case/(_ x): h => y /hle.
  by rewrite leNgt => /negbTE ->.
move/forallNP => h x; have {h} := h x.
move=> /ubP /existsNP => -[y /not_implyP[Ey /negP]].
by rewrite -ltNge => ltx; exists y.
Qed.

Lemma

has_lbPn

---

Source code

E

---

Source code

: ~ has_lbound E <-> (forall

x

---

Source code

, exists2

y

---

Source code

, E y & y < x).

Proof.

split=> [/has_lb_ubN /has_ubPn NEnub x|Enlb /has_lb_ubN].
  have [y ENy ltxy] := NEnub (- x); exists (- y); rewrite 1?ltrNl //.
  by case: ENy => z Ez <-; rewrite opprK.
apply/has_ubPn => x; have [y Ey ltyx] := Enlb (- x).
exists (- y); last by rewrite ltrNr.
by exists y => //; rewrite opprK.
Qed.

Lemma

hasNlbound_itv

---

Source code

(

a

---

Source code

: itv_bound R) : a != -oo%O ->
  ~ has_lbound [set` Interval -oo%O a].

Proof.

move: a => [b r|[|]] _ //.
  suff: ~ has_lbound `]-oo, r[%classic.
    by case: b => //; apply/contra_not/subset_has_lbound => x /ltW.
  apply/has_lbPn => x; exists (minr (r - 1) (x - 1)).
    by rewrite !set_itvE/= gt_min ltrBlDr ltrDl ltr01.
  by rewrite gt_min orbC ltrBlDr ltrDl ltr01.
case=> r /(_ (r - 1)) /=; rewrite in_itv /= => /(_ erefl).
by apply/negP; rewrite -ltNge ltrBlDr ltrDl.
Qed.

Lemma

hasNubound_itv

---

Source code

(

a

---

Source code

: itv_bound R) : a != +oo%O ->
  ~ has_ubound [set` Interval a +oo%O].

Proof.

move: a => [b r|[|]] _ //.
  suff: ~ has_ubound `]r, +oo[%classic.
    case: b => //; apply/contra_not/subset_has_ubound => x.
    by rewrite !set_itvE => /ltW.
  apply/has_ubPn => x; rewrite !set_itvE; exists (maxr (r + 1) (x + 1));
  by rewrite ?in_itv /= ?andbT lt_max ltrDl ltr01 // orbT.
case=> r /(_ (r + 1)) /=; rewrite in_itv /= => /(_ erefl).
by apply/negP; rewrite -ltNge ltrDl.
Qed.

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_bndy

---

Source code

(

R

---

Source code

: numDomainType) (

x

---

Source code

: R)

b

---

Source code

:
  -%R @` [set` Interval (BSide b x) +oo%O] =
  [set` Interval -oo%O (BSide (negb b) (- x))].

Proof.

rewrite predeqE => /= r; split=> [[y xy <-]|xr].
  by case: b xy; rewrite !in_itv/= andbT (lerN2, ltrN2).
exists (- r); rewrite ?opprK //.
by case: b xr; rewrite !in_itv/= andbT (lerNr, ltrNr).
Qed.

Lemma

opp_itvNy_bnd

---

Source code

(

R

---

Source code

: numDomainType) (

x

---

Source code

: R)

b

---

Source code

:
  -%R @` [set` Interval -oo%O (BSide b x)] =
  [set` Interval (BSide (negb b) (- x)) +oo%O].

Proof.

rewrite predeqE => /= r; split=> [[y xy <-]|xr].
  by case: b xy; rewrite !in_itv/= andbT (lerN2, ltrN2).
exists (- r); rewrite ?opprK //.
by case: b xr; rewrite !in_itv/= andbT (lerNl, ltrNl).
Qed.

Lemma

opp_itv_bnd_bnd

---

Source code

(

R

---

Source code

: numDomainType)

a

---

Source code

b

---

Source code

(

x

---

Source code

y

---

Source code

: R) :
  -%R @` [set` Interval (BSide a x) (BSide b y)] =
  [set` Interval (BSide (~~ b) (- y)) (BSide (~~ a) (- x))].

Proof.

rewrite predeqE => /= r; split => [[{}r + <-]|].
  by rewrite !in_itv/= 2!lteifN2 negbK andbC.
rewrite in_itv/= negbK => yrab.
by exists (- r); rewrite ?opprK// !in_itv lteifNr andbC lteifNl.
Qed.

Lemma

opp_itvoo

---

Source code

(

R

---

Source code

: numDomainType) (

x

---

Source code

y

---

Source code

: R) :
  -%R @` `]x, y[%classic = `](- y), (- x)[%classic.

Proof.

rewrite predeqE => /= r; split => [[{}r + <-]|].
  by rewrite !in_itv/= !ltrN2 andbC.
by exists (- r); rewrite ?opprK// !in_itv/= ltrNl ltrNr andbC.
Qed.

Lemma

opp_preimage_itvbndy

---

Source code

(

R

---

Source code

: numDomainType)

ba

---

Source code

(

a

---

Source code

: R) (

bb

---

Source code

: bool):
  -%R @^-1` [set` Interval (BSide ba a) (BInfty _ bb)] =
  [set` Interval (BInfty _ (~~ bb)) (BSide (~~ ba) (- a))].

Proof.

by apply/seteqP; split => [x/=|x/=]; rewrite oppr_itvy. Qed.

Lemma

opp_preimage_itvbndbnd

---

Source code

(

R

---

Source code

: numDomainType)

ba

---

Source code

(

a

---

Source code

: R)

bb

---

Source code

(

b

---

Source code

: R) :
  -%R @^-1` [set` Interval (BSide ba a) (BSide bb b)] =
  [set` Interval (BSide (~~ bb) (- b)) (BSide (~~ ba) (- a))].

Proof.

by apply/seteqP; split => [x/=|x/=]; rewrite oppr_itv. Qed.

Section set_itv_porderType.
Context {

d

---

Source code

} {

T

---

Source code

: porderType d}.
Implicit Types (a : itv_bound T) (x y : T) (i j : interval T) (b : bool).

Lemma

set_itv_splitI

---

Source code

i

---

Source code

: [set` i] = [set` Interval i.1 +oo%O] `&` [set` Interval -oo%O i.2].

Proof.

case: i => [a a']; apply/predeqP=> x/=.
by rewrite [in X in X <-> _]itv_splitI (rwP andP).
Qed.

End set_itv_porderType.

Section set_itv_orderType.
Context {

d

---

Source code

} {

T

---

Source code

: orderType d}.
Implicit Types (a : itv_bound T) (x y : T) (i j : interval T) (b : bool).

Lemma

setCitvl

---

Source code

a

---

Source code

: ~` [set` Interval -oo%O a] = [set` Interval a +oo%O].

Proof.

by apply/predeqP => y /=; rewrite -predC_itvl (rwP negP). Qed.

Lemma

setCitvr

---

Source code

a

---

Source code

: ~` [set` Interval a +oo%O] = [set` Interval -oo%O a].

Proof.

by rewrite -setCitvl setCK. Qed.

Lemma

setCitv

---

Source code

i

---

Source code

:
  ~` [set` i] = [set` Interval -oo%O i.1] `|` [set` Interval i.2 +oo%O].

Proof.

by apply/predeqP => x /=; rewrite (rwP orP) (rwP negP) [x \notin i]predC_itv.
Qed.

Lemma

set_itv_splitD

---

Source code

i

---

Source code

:
  [set` i] = [set` Interval i.1 +oo%O] `\` [set` Interval i.2 +oo%O].

Proof.

by rewrite set_itv_splitI/= setDE setCitvr. Qed.

Lemma

itv_setU_setT

---

Source code

b

---

Source code

x

---

Source code

:
  [set` Interval -oo%O (BSide b x)] `|`
  [set` Interval (BSide b x) +oo%O] = [set: T].

Proof.

by rewrite -itv_bndbnd_setU// set_itvE. Qed.

End set_itv_orderType.

Section line_path_factor_numDomainType.
Context {

R

---

Source code

: numDomainType}.
Implicit Types (a b t r : R) (A : set R).

Lemma

memB_itv

---

Source code

(

x

---

Source code

y

---

Source code

: bool)

a

---

Source code

b

---

Source code

t

---

Source code

:
  (b - t \in Interval (BSide x a) (BSide y b)) =
  (a + t \in Interval (BSide (~~ y) a) (BSide (~~ x) b)).

Proof.

rewrite !in_itv/= /Order.lteif !if_neg.
by rewrite gerBl gtrBl lerDl ltrDl lerBrDr ltrBrDr andbC.
Qed.

Lemma

memB_itv0

---

Source code

(

x

---

Source code

y

---

Source code

: bool) (

a

---

Source code

b

---

Source code

: R) :
  (b - a \in Interval (BSide x 0) (BSide y b)) =
  (a \in Interval (BSide (~~ y) 0) (BSide (~~ x) b)).

Proof.

by rewrite memB_itv add0r. Qed.

Lemma

__deprepcated__mem_1B_itvcc

---

Source code

t

---

Source code

: (1 - t \in `[0, 1]) = (t \in `[0, 1]).

Proof.

exact: memB_itv0. Qed.

Definition

line_path

prod_filter_on : forall [T U : Type], filter_on T -> filter_on U -> filter_on (T * U) prod_filter_on is not universe polymorphic Arguments prod_filter_on [T U]%_type_scope F G prod_filter_on is transparent Expands to: Constant mathcomp.classical.filter.prod_filter_on Declared in library mathcomp.classical.filter, line 1050, characters 10-24

---

Source code

a

---

Source code

b

---

Source code

t

---

Source code

: R := (1 - t) * a + t * b.

Lemma

line_path_id

---

Source code

: line_path 0 1 = id.

Proof.

by apply/funext => t; rewrite /line_path mulr0 add0r mulr1. Qed.

Lemma

line_pathEl

---

Source code

a

---

Source code

b

---

Source code

t

---

Source code

: line_path a b t = t * (b - a) + a.

Proof.

by rewrite /line_path mulrBl addrAC -addrA -mulrBr mul1r addrC. Qed.

Lemma

line_pathEr

---

Source code

a

---

Source code

b

---

Source code

t

---

Source code

: line_path a b t = (1 - t) * (a - b) + b.

Proof.

by rewrite mulrBl mul1r addrAC subrK -mulrN opprB addrC line_pathEl. Qed.

Lemma

line_path10

---

Source code

t

---

Source code

: line_path 1 0 t = 1 - t.

Proof.

by rewrite /line_path mulr0 addr0 mulr1. Qed.

Lemma

line_path0

---

Source code

a

---

Source code

b

---

Source code

: line_path a b 0 = a.

Proof.

by rewrite /line_path subr0 mul1r mul0r addr0. Qed.

Lemma

line_path1

---

Source code

a

---

Source code

b

---

Source code

: line_path a b 1 = b.

Proof.

by rewrite /line_path subrr mul0r add0r mul1r. Qed.

Lemma

line_path_sym

---

Source code

a

---

Source code

b

---

Source code

t

---

Source code

: line_path a b t = line_path b a (1 - t).

Proof.

by rewrite /line_path subKr addrC. Qed.

Lemma

line_path_flat

---

Source code

a

---

Source code

: line_path a a = cst a.

Proof.

by apply/funext => t; rewrite line_pathEl subrr mulr0 add0r. Qed.

Lemma

leW_line_path

---

Source code

a

---

Source code

b

---

Source code

: a <= b -> {homo line_path a b :

x

---

Source code

y

---

Source code

/ x <= y}.

Proof.

by move=> ? ? ? ?; rewrite !line_pathEl lerD ?ler_wpM2r// subr_ge0.
Qed.

Definition

factor

in_filter_prod : forall {T U : Type} {F : set_system T} {G : set_system U}, in_filter (T:=T) F -> in_filter (T:=U) G -> in_filter (T:=T * U) (filter_prod F G) in_filter_prod is not universe polymorphic Arguments in_filter_prod {T U}%_type_scope {F G} P Q in_filter_prod is transparent Expands to: Constant mathcomp.classical.filter.in_filter_prod Declared in library mathcomp.classical.filter, line 1076, characters 19-33

---

Source code

a

---

Source code

b

---

Source code

x

---

Source code

:= (x - a) / (b - a).

Lemma

leW_factor

---

Source code

a

---

Source code

b

---

Source code

: a <= b -> {homo factor a b :

x

---

Source code

y

---

Source code

/ x <= y}.

Proof.

by move=> ? ? ? ?; rewrite /factor ler_wpM2r ?lerD// invr_ge0 subr_ge0.
Qed.

Lemma

factor_flat

---

Source code

a

---

Source code

: factor a a = cst 0.

Proof.

by apply/funext => x; rewrite /factor subrr invr0 mulr0. Qed.

Lemma

factorl

---

Source code

a

---

Source code

b

---

Source code

: factor a b a = 0.

Proof.

by rewrite /factor subrr mul0r. Qed.

Definition

ndline_path

near_simpl : (forall (U : Type) (T : filteredType U) (x : T) (P : set U), (\forall x0 \near nbhs x, P x0) = (\near x, P x)) * (forall (U : Type) (T : filteredType U) (x : T) (P : set U), nbhs x P = (\near x, P x)) * (forall (X : Type) (fX : filteredType X) (x : fX) (P : set X), nbhs x P = (\near x, P x)) * (forall (T : Type) (F : filter_on T) (P : set T), (\near F, P F) = (\forall x \near F, P x)) * (forall (T U : Type) (f : T -> U) (F : set_system T) (P : set U), (\forall y \near (f x @[x --> F])%classic, P y) = (\near F, P (f F))) * (forall (T U : Type) (f : T -> set U) (F : set_system T) (P : set U), (\forall y \near (f x `@[x --> F])%classic, P y) = (\near F, exists y : U, f F y /\ P y)) * (forall (T T' U U' : Type) (f : T -> U) (g : T' -> U') (F : set_system T) (G : set_system T') (P : U -> set U'), Filter F -> Filter G -> (\forall y \near (f x @[x --> F])%classic & y' \near (g x @[x --> G])%classic, P y y') = (\near F & G, P (f F) (g G))) near_simpl is not universe polymorphic near_simpl is transparent Expands to: Constant mathcomp.classical.filter.NearMap.near_simpl Declared in library mathcomp.classical.filter, line 1146, characters 11-21

---

Source code

a

---

Source code

b

---

Source code

& a < b := line_path a b.

Lemma

ndline_pathE

---

Source code

a

---

Source code

b

---

Source code

(

ab

---

Source code

: a < b) : ndline_path ab = line_path a b.

Proof.

by []. Qed.

End line_path_factor_numDomainType.
#[deprecated(since="mathcomp-analysis 1.12.0", note="use `memB_itv0` instead")]
Notation

mem_1B_itvcc

---

Source code

:= __deprepcated__mem_1B_itvcc (only parsing).

Section line_path_factor_numFieldType.
Context {

R

---

Source code

: numFieldType}.
Implicit Types (a b t r : R) (A : set R).

Lemma

factorr

---

Source code

a

---

Source code

b

---

Source code

: a != b -> factor a b b = 1.

Proof.

by move=> Nab; rewrite /factor divff// subr_eq0 eq_sym. Qed.

Lemma

factorK

---

Source code

a

---

Source code

b

---

Source code

: a != b -> cancel (factor a b) (line_path a b).

Proof.

by move=> ? x; rewrite line_pathEl mulfVK ?addrNK// subr_eq0 eq_sym. Qed.

Lemma

line_pathK

---

Source code

a

---

Source code

b

---

Source code

: a != b -> cancel (line_path a b) (factor a b).

Proof.

by move=> ? x; rewrite /factor line_pathEl addrK mulfK// subr_eq0 eq_sym.
Qed.

Lemma

line_path_inj

---

Source code

a

---

Source code

b

---

Source code

: a != b -> injective (line_path a b).

Proof.

by move/line_pathK/can_inj. Qed.

Lemma

factor_inj

---

Source code

a

---

Source code

b

---

Source code

: a != b -> injective (factor a b).

Proof.

by move/factorK/can_inj. Qed.

Lemma

line_path_bij

---

Source code

a

---

Source code

b

---

Source code

: a != b -> bijective (line_path a b).

Proof.

by move=> ab; apply: Bijective (line_pathK ab) (factorK ab). Qed.

Lemma

factor_bij

---

Source code

a

---

Source code

b

---

Source code

: a != b -> bijective (factor a b).

Proof.

by move=> ab; apply: Bijective (factorK ab) (line_pathK ab). Qed.

Lemma

le_line_path

---

Source code

a

---

Source code

b

---

Source code

: a < b -> {mono line_path a b :

x

---

Source code

y

---

Source code

/ x <= y}.

Proof.

move=> ltab; have leab := ltW ltab.
apply: homo_mono (line_pathK _) (leW_factor _) (leW_line_path _) => //.
by rewrite lt_eqF.
Qed.

Lemma

le_factor

---

Source code

a

---

Source code

b

---

Source code

: a < b -> {mono factor a b :

x

---

Source code

y

---

Source code

/ x <= y}.

Proof.

move=> ltab; have leab := ltW ltab.
apply: homo_mono (factorK _) (leW_line_path _) (leW_factor _) => //.
by rewrite lt_eqF.
Qed.

Lemma

lt_line_path

---

Source code

a

---

Source code

b

---

Source code

: a < b -> {mono line_path a b :

x

---

Source code

y

---

Source code

/ x < y}.

Proof.

by move/le_line_path/leW_mono. Qed.

Lemma

lt_factor

---

Source code

a

---

Source code

b

---

Source code

: a < b -> {mono factor a b :

x

---

Source code

y

---

Source code

/ x < y}.

Proof.

by move/le_factor/leW_mono. Qed.

Let

ltNeq

---

Source code

a

---

Source code

b

---

Source code

: a < b -> a != b

Proof.

by move=> /lt_eqF->. Qed.

HB

---

Source code

.

instance

---

Source code

Definition

---

Source code

_

---

Source code

a

---

Source code

b

---

Source code

(

ab

---

Source code

:

---

Source code

a

---

Source code

< b) :=
  @Can2.Build _ _ setT setT (ndline_path ab) (factor a b)
    (fun _ _ => I) (fun _ _ => I)
    (in1W (line_pathK (ltNeq ab))) (in1W (factorK (ltNeq ab))).

Lemma

line_path_itv_bij

---

Source code

ba

---

Source code

bb

---

Source code

a

---

Source code

b

---

Source code

: a < b ->
  set_bij [set` Interval (BSide ba 0) (BSide bb 1)]
          [set` Interval (BSide ba a) (BSide bb b)] (line_path a b).

Proof.

move=> ltab; rewrite -ndline_pathE.
apply: bij_subr => //=; rewrite setTI ?ndline_pathE.
apply/predeqP => t /=; rewrite !in_itv/= {1}line_pathEl line_pathEr.
rewrite -lteifBlDr subrr -lteif_pdivrMr ?subr_gt0// mul0r.
rewrite -lteifBrDr subrr -lteif_ndivrMr ?subr_lt0// mul0r.
by rewrite lteifBrDl addr0.
Qed.

Lemma

factor_itv_bij

---

Source code

ba

---

Source code

bb

---

Source code

a

---

Source code

b

---

Source code

: a < b ->
  set_bij [set` Interval (BSide ba a) (BSide bb b)]
          [set` Interval (BSide ba 0) (BSide bb 1)] (factor a b).

Proof.

move=> ltab; have -> : factor a b = (ndline_path ltab)^-1%FUN by [].
by apply/splitbij_sub_sym => //; apply: line_path_itv_bij.
Qed.

Lemma

mem_line_path_itv

---

Source code

ba

---

Source code

bb

---

Source code

a

---

Source code

b

---

Source code

: a < b ->
  set_fun [set` Interval (BSide ba 0) (BSide bb 1)]
          [set` Interval (BSide ba a) (BSide bb b)] (line_path a b).

Proof.

by case/(line_path_itv_bij ba bb). Qed.

Lemma

mem_line_path_itvcc

---

Source code

a

---

Source code

b

---

Source code

: a <= b -> set_fun `[0, 1] `[a, b] (line_path a b).

Proof.

rewrite le_eqVlt => /predU1P[<-|]; first by rewrite set_itv1 line_path_flat.
by move=> lt_ab; case: (line_path_itv_bij true false lt_ab).
Qed.

Lemma

range_line_path

---

Source code

ba

---

Source code

bb

---

Source code

a

---

Source code

b

---

Source code

: a < b ->
   line_path a b @` [set` Interval (BSide ba 0) (BSide bb 1)] =
               [set` Interval (BSide ba a) (BSide bb b)].

Proof.

by move=> /(line_path_itv_bij ba bb)/Pbij[f ->]; rewrite image_eq. Qed.

Lemma

range_factor

---

Source code

ba

---

Source code

bb

---

Source code

a

---

Source code

b

---

Source code

: a < b ->
   factor a b @` [set` Interval (BSide ba a) (BSide bb b)] =
                 [set` Interval (BSide ba 0) (BSide bb 1)].

Proof.

by move=> /(factor_itv_bij ba bb)/Pbij[f ->]; rewrite image_eq. Qed.

Lemma

onem_factor

---

Source code

a

---

Source code

b

---

Source code

x

---

Source code

: a != b -> (factor a b x).~ = factor b a x.

Proof.

rewrite eq_sym -subr_eq0 => ab; rewrite /onem /factor -(divff ab) -mulrBl.
by rewrite opprB addrA subrK -mulrNN opprB -invrN opprB.
Qed.

End line_path_factor_numFieldType.

Lemma

mem_factor_itv

---

Source code

(

R

---

Source code

: realFieldType)

ba

---

Source code

bb

---

Source code

(

a

---

Source code

b

---

Source code

: R) :
  set_fun [set` Interval (BSide ba a) (BSide bb b)]
          [set` Interval (BSide ba 0) (BSide bb 1)] (factor a b).

Proof.

have [|leba] := ltP a b; first by case/(factor_itv_bij ba bb).
move=> x /=; have [|/itv_ge->//] := (boolP (BSide ba a < BSide bb b)%O).
rewrite lteBSide; case: ba bb => [] []//=; rewrite ?le_gtF//.
by case: ltgtP leba => // -> _ _ _; rewrite factor_flat in_itv/= lexx ler01.
Qed.

Lemma

neitv_bnd1

---

Source code

(

R

---

Source code

: numFieldType) (

s

---

Source code

: seq (interval R)) :
  all neitv s -> forall

i

---

Source code

, i \in s -> i.1 != +oo%O.

Proof.

move=> /allP sne [a b] si /=; apply/negP => /eqP boo; move: si.
by rewrite boo => /sne /negP; apply; rewrite set_itv_infty_set0.
Qed.

Lemma

neitv_bnd2

---

Source code

(

R

---

Source code

: numFieldType) (

s

---

Source code

: seq (interval R)) :
  all neitv s -> forall

i

---

Source code

, i \in s -> i.2 != -oo%O.

Proof.

move=> /allP sne [a b] si /=; apply/negP => /eqP boo; move: si.
by rewrite boo => /sne /negP; apply; rewrite set_itv_infty_set0.
Qed.

Lemma

trivIset_set_itv_nth

---

Source code

(

R

---

Source code

: numDomainType)

def

---

Source code

(

s

---

Source code

: seq (interval R))
  (

D

---

Source code

: set nat) : [set` def] = set0 ->
  trivIset D (fun

i

---

Source code

=> [set` nth def s i]) <->
    trivIset D (fun

i

---

Source code

=> nth set0 [seq [set` j] |

j

---

Source code

<- s] i).

Proof.

move=> def0; split=> /trivIsetP ss; apply/trivIsetP => i j Di Dj ij.
- have [si|si] := ltP i (size s); last first.
    by rewrite (nth_default set0) ?size_map// set0I.
  have [sj|sj] := ltP j (size s); last first.
    by rewrite setIC (nth_default set0) ?size_map// set0I.
  by rewrite (nth_map def) // (nth_map def) // ss.
- have [?|h] := ltP i (size s); last by rewrite (nth_default def h) def0 set0I.
  have [?|h] := ltP j (size s); last by rewrite (nth_default def h) def0 setI0.
  by have := ss _ _ Di Dj ij; rewrite (nth_map def) // (nth_map def).
Qed.

Arguments trivIset_set_itv_nth {R} _ {s}.

Section disjoint_itv.
Context {

disp

---

Source code

: Order.disp_t} {

T

---

Source code

: porderType disp}.

Definition

disjoint_itv

cvg_to_comp_2 : forall [T U V W : Type] [F : set_system T] [G : set_system U] [H : set_system V] [I : set_system W], Filter F -> Filter G -> Filter H -> forall [f : T -> U] [g : T -> V] [h : U -> V -> W], (f x @[x --> F] --> G)%classic -> (g x @[x --> F] --> H)%classic -> (h x.1 x.2 @[x --> (G, H)] --> I)%classic -> (h (f x) (g x) @[x --> F] --> I)%classic cvg_to_comp_2 is not universe polymorphic Expanded type for implicit arguments cvg_to_comp_2 : forall [T U V W : Type] [F : set_system T] [G : set_system U] [H : set_system V] [I : set_system W], Filter F -> Filter G -> Filter H -> forall [f : T -> U] [g : T -> V] [h : U -> V -> W], (f x @[x --> F] --> G)%classic -> (g x @[x --> F] --> H)%classic -> (h x.1 x.2 @[x --> (G, H)] --> I)%classic -> forall [t : set W], nbhs I t -> F ((fun x : T => h (f x) (g x)) @^-1` t)%classic Arguments cvg_to_comp_2 [T U V W]%_type_scope [F G H I] FF FG FH [f g h]%_function_scope _ _ _ [t] _ cvg_to_comp_2 is transparent Expands to: Constant mathcomp.classical.filter.cvg_to_comp_2 Declared in library mathcomp.classical.filter, line 1172, characters 11-24

---

Source code

: rel (interval T) :=
  fun

a

---

Source code

b

---

Source code

=> [disjoint [set` a] & [set` b]].

Lemma

disjoint_itvxx

---

Source code

(

i

---

Source code

: interval T) : neitv i -> ~~ disjoint_itv i i.

Proof.

by move=> i0; rewrite /disjoint_itv/= /disj_set /= setIid. Qed.

Lemma

disjoint_rays

---

Source code

b

---

Source code

(

x

---

Source code

: T) :
  disjoint_itv (Interval -oo%O (BSide b x)) (Interval (BSide b x) +oo%O).

Proof.

by rewrite eq_opE -(set_itvxx (BSide b x)) [RHS]set_itv_splitI setIC. Qed.

End disjoint_itv.

Section disjoint_itv_orderType.
Context {

disp

---

Source code

: Order.disp_t} {

T

---

Source code

: orderType disp}.

Lemma

disjoint_neitv

---

Source code

(

i

---

Source code

j

---

Source code

: interval T) :
  disjoint_itv i j <-> ~~ neitv (itv_meet i j).

Proof.

case: i j => [a b] [c d]; rewrite /disjoint_itv/disj_set /= -set_itvI.
by split => [/negPn//|?]; apply/negPn.
Qed.

End disjoint_itv_orderType.

Section disjoint_itv_numDomain.

Context {

R

---

Source code

: numDomainType}.

Import Order.Theory.

Lemma

lt_disjoint

---

Source code

(

i

---

Source code

j

---

Source code

: interval R) :
  (forall

x

---

Source code

y

---

Source code

, x \in i -> y \in j -> x < y) -> disjoint_itv i j.

Proof.

move=> ij; apply/eqP; rewrite predeqE => x; split => // -[xi xj].
by have := ij _ _ xi xj; rewrite ltxx.
Qed.

End disjoint_itv_numDomain.

Section open_endpoints.
Context {

d

---

Source code

} {

T

---

Source code

: porderType d}.
Implicit Types (i : interval T).

Definition

is_open_itv

within_filter_on : forall [T : Type], set T -> filter_on T -> filter_on T within_filter_on is not universe polymorphic Arguments within_filter_on [T]%_type_scope D%_classical_set_scope F within_filter_on is transparent Expands to: Constant mathcomp.classical.filter.within_filter_on Declared in library mathcomp.classical.filter, line 1240, characters 10-26

---

Source code

(

A

---

Source code

: set T) := exists

ab

---

Source code

, A = `]ab.1, ab.2[%classic.

Definition

open_itv_cover

subset_filter : forall [T : finType] (p : T -> bool) [s1 s2 : seq T], s1 \subset s2 -> [seq a <- s1 | p a] \subset [seq a <- s2 | p a] subset_filter is not universe polymorphic Arguments subset_filter [T] p%_function_scope [s1 s2]%_seq_scope _ subset_filter is opaque Expands to: Constant mathcomp.boot.fintype.subset_filter Declared in library mathcomp.boot.fintype, line 710, characters 6-19

---

Source code

(

A

---

Source code

: set T) := [set

F

---

Source code

: nat -> set T |
  (forall

k

---

Source code

, is_open_itv (F k)) /\ A `<=` \bigcup_

k

---

Source code

(F k)].

Definition

itv_is_open_unbounded

powerset_filter_from : forall {Y : Type}, set_system Y -> set_system (set Y) powerset_filter_from is not universe polymorphic Arguments powerset_filter_from {Y}%_type_scope F _ powerset_filter_from is transparent Expands to: Constant mathcomp.classical.filter.powerset_filter_from Declared in library mathcomp.classical.filter, line 1285, characters 11-31

---

Source code

i

---

Source code

: bool :=
  match i with
  | `]-oo, _[ | `]_, +oo[ | `]-oo, +oo[ => true
  | _ => false
  end.

Definition

itv_is_oo

principal_filter : forall {X : Type}, X -> set_system X principal_filter is not universe polymorphic Arguments principal_filter {X}%_type_scope x _ principal_filter is transparent Expands to: Constant mathcomp.classical.filter.principal_filter Declared in library mathcomp.classical.filter, line 1378, characters 11-27

---

Source code

i

---

Source code

: bool := if i is `]_, _[ then true else false.

Definition

itv_open_ends

principal_filter_type : Type -> Type principal_filter_type is not universe polymorphic Arguments principal_filter_type P%_type_scope principal_filter_type is transparent Expands to: Constant mathcomp.classical.filter.principal_filter_type Declared in library mathcomp.classical.filter, line 1382, characters 11-32

---

Source code

i

---

Source code

: bool := itv_is_open_unbounded i || itv_is_oo i.

Lemma

itv_open_ends_rside

---

Source code

l

---

Source code

b

---

Source code

(

t

---

Source code

: T) :
  itv_open_ends (Interval l (BSide b t)) -> b = true.

Proof.

by case: b; move: l => [[]?|[]] // [] //. Qed.

Lemma

itv_open_ends_rinfty

---

Source code

l

---

Source code

b

---

Source code

:
  itv_open_ends (Interval l (BInfty T b)) -> b = false.

Proof.

by case: b => //; move: l => [[]?|[]] // []. Qed.

Lemma

itv_open_ends_lside

---

Source code

l

---

Source code

b

---

Source code

(

t

---

Source code

: T) :
  itv_open_ends (Interval (BSide b t) l) -> b = false.

Proof.

by case: b; move: l => [[]?|[]] // []. Qed.

Lemma

itv_open_ends_linfty

---

Source code

l

---

Source code

b

---

Source code

:
  itv_open_ends (Interval (BInfty T b) l) -> b = true.

Proof.

by case: b => //; move: l => [[]?|[]] // []. Qed.

Lemma

is_open_itv_itv_is_bd_openP

---

Source code

i

---

Source code

: itv_is_oo i -> is_open_itv [set` i].

Proof.

by case: i=> [] [[]l|[]] // [[]r|[]] // ?; exists (l,r). Qed.

End open_endpoints.

Section closed_endpoints.
Context {

d

---

Source code

} {

T

---

Source code

: porderType d}.
Implicit Types (i : interval T).

Definition

itv_is_closed_unbounded

filterI_iter : forall {T : Type}, set_system T -> nat -> set (set T) filterI_iter is not universe polymorphic Arguments filterI_iter {T}%_type_scope F n%_nat_scope _ filterI_iter is transparent Expands to: Constant mathcomp.classical.filter.filterI_iter Declared in library mathcomp.classical.filter, line 1530, characters 9-21

---

Source code

i

---

Source code

: bool :=
  match i with
  | `[_, +oo[ | `]-oo, _] | `]-oo, +oo[ => true
  | _ => false
  end.

Definition

itv_is_cc

open_finI_from : forall [I : choiceType] [T : Type], set I -> (I -> set T) -> set (set T) open_finI_from is not universe polymorphic Arguments open_finI_from [I] [T]%_type_scope D%_classical_set_scope f%_function_scope _ open_finI_from is transparent Expands to: Constant mathcomp.classical.filter.open_finI_from Declared in library mathcomp.classical.filter, line 1562, characters 11-25

---

Source code

i

---

Source code

: bool := if i is `[_, _] then true else false.

Definition

itv_closed_ends

finI : forall [I : choiceType] [T : Type], set I -> (I -> set T) -> Prop finI is not universe polymorphic Arguments finI [I] [T]%_type_scope D%_classical_set_scope f%_function_scope finI is transparent Expands to: Constant mathcomp.classical.filter.finI Declared in library mathcomp.classical.filter, line 1635, characters 11-15

---

Source code

i

---

Source code

: bool := itv_is_closed_unbounded i || itv_is_cc i.

End closed_endpoints.

Lemma

itv_open_endsI

---

Source code

{

d

---

Source code

} {

T

---

Source code

: orderType d} (

i

---

Source code

j

---

Source code

: interval T) :
  itv_open_ends i -> itv_open_ends j -> itv_open_ends (i `&` j)%O.

Proof.

by move: i => [][[]a|[]] [[]b|[]]//=; move: j => [][[]x|[]] [[]y|[]]//=;
   rewrite /itv_open_ends/= ?orbF ?andbT -?negb_or ?le_total//=.
Qed.

Lemma

itv_setU

---

Source code

{

d

---

Source code

} {

T

---

Source code

: orderType d} (

i

---

Source code

j

---

Source code

: interval T) :
  [set` i] `&` [set` j] !=set0 -> [set` (i `|` j)%O] = [set` i] `|` [set` j].

Proof.

case=> p [ip jp]; have pij : p \in (i `|` j)%O by exact/(le_trans ip)/leUl.
move: i j ip jp pij => [x y] [a b] /andP[xp py] /andP[ap pb] pab.
rewrite eqEsubset; split => /= r /=; first last.
  by move=> -[ra|rb]; [exact/(le_trans ra)/leUl|exact/(le_trans rb)/leUr].
rewrite (@itv_splitUeq _ T p (x `&` a)%O)// => /orP[].
- move=> /andP[xar rp]; have /orP[ax|xa] := le_total a x.
  + right; apply/andP; split; first by rewrite (le_trans _ xar)// leIidr.
    by rewrite (le_trans rp)// (le_trans _ pb)// bnd_simp.
  + left; apply/andP; split; first by rewrite (le_trans _ xar)// leIidl.
    by rewrite (le_trans rp)// (le_trans _ py)//= bnd_simp.
- move=> /predU1P[->|/andP[pr ryb]]; first by left; apply/andP.
  have /orP[bly|ylb] := le_total b y.
  + left; apply/andP; split; last by rewrite (le_trans ryb)// leUidr.
    by rewrite (le_trans _ pr)// (le_trans xp)//= bnd_simp.
  + right; apply/andP; split; last by rewrite (le_trans ryb)// leUidl.
    by rewrite (le_trans ap)// (le_trans _ pr)//= bnd_simp.
Qed.

Lemma

itv_setI

---

Source code

{

d

---

Source code

} {

T

---

Source code

: orderType d} (

i

---

Source code

j

---

Source code

: interval T) :
  [set` (i `&` j)%O] = [set` i] `&` [set` j].

Proof.

by rewrite eqEsubset; split => z; rewrite /in_mem/= /pred_of_itv/= lexI=> /andP.
Qed.