Library mathcomp.analysis.classical_sets

(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From mathcomp Require Import all_ssreflect ssralg matrix finmap order ssrnum.
From mathcomp Require Import ssrint interval.
Require Import mathcomp_extra boolp.

This file develops a basic theory of sets and types equipped with a canonical inhabitant (pointed types). --> A decidable equality is defined for any type. It is thus possible to define an eqType structure for any type using the mixin gen_eqMixin. > This file adds the possibility to define a choiceType structure for any type thanks to an axiom gen_choiceMixin giving a choice mixin. > We chose to have generic mixins and no global instances of the eqType and choiceType structures to let the user choose which definition of equality to use and to avoid conflict with already declared instances.

Sets:

set T == type of sets on T. (x \in P) == boolean membership predicate from ssrbool for set P, available thanks to a canonical predType T structure on sets on T. [set x : T | P] == set of points x : T such that P holds. [set x | P] == same as before with T left implicit. [set E | x in A] == set defined by the expression E for x in set A. [set E | x in A & y in B] == same as before for E depending on 2 variables x and y in sets A and B. setT == full set. set0 == empty set. range f == the range of f, i.e. [set f x | x in setT] [set a] == set containing only a. [set a : T] == same as before with the type of a made explicit. A `|` B == union of A and B. a |` A == A extended with a. [set a1; a2; ..; an] == set containing only the n elements ai. A `&` B == intersection of A and B. A `*` B == product of A and B, i.e. set of pairs (a,b) such that A a and B b. A.`1 == set of points a such that there exists b so that A (a, b). A.`2 == set of points a such that there exists b so that A (b, a). ~` A == complement of A. [set~ a] == complement of [set a]. A `\` B == complement of B in A. A `\ a == A deprived of a. \bigcup(i in P) F == union of the elements of the family F whose index satisfies P. \bigcup(i : T) F == union of the family F indexed on T. \bigcup_i F == same as before with T left implicit. \bigcap(i in P) F == intersection of the elements of the family F whose index satisfies P. \bigcap(i : T) F == union of the family F indexed on T. \bigcap_i F == same as before with T left implicit. smallest C G := \bigcap(A in [set M | C M /\ G `<=` M]) A A `<=` B <-> A is included in B. A `<=>` B <-> double inclusion A `<=` B and B `<=` A. f @^-1` A == preimage of A by f. f @` A == image of A by f. Notation for `image A f`. A !=set0 := exists x, A x. [set` p] == a classical set corresponding to the predType p ` [a, b] := [set` ` [a, b] ], i.e., a classical set corresponding to the interval ` [a, b]. ` ]a, b] := [set` ` ]a, b] ] ` [a, b[ := [set` ` [a, b[ ] ` ]a, b[ := [set` ` ]a, b[ ] ` ]-oo, b] := [set` ` ]-oo, b] ] ` ]-oo, b[ := [set` ` ]-oo, b[ ] ` [a, +oo[ := [set` ` [a, +oo[ ] ` ]a, +oo[ := [set` ` ]a, +oo[ ] ` ]-oo, +oo[ := [set` ` ]-oo, +oo[ ] `I_n := [set k | k < n] is_subset1 A <-> A contains only 1 element. is_fun f <-> for each a, f a contains only 1 element. is_total f <-> for each a, f a is non empty. is_totalfun f <-> conjunction of is_fun and is_total. xget x0 P == point x in P if it exists, x0 otherwise; P must be a set on a choiceType. fun_of_rel f0 f == function that maps x to an element of f x if there is one, to f0 x otherwise. F `#` G <-> intersections beween elements of F an G are all non empty.

Pointed types:

pointedType == interface type for types equipped with a canonical inhabitant. PointedType T m == packs the term m : T to build a pointedType; T must have a choiceType structure. [pointedType of T for cT] == T-clone of the pointedType structure cT. [pointedType of T] == clone of a canonical pointedType structure on T. point == canonical inhabitant of a pointedType. get P == point x in P if it exists, point otherwise; P must be a set on a pointedType. --> Thanks to this basic set theory, we proved Zorn's Lemma, which states that any ordered set such that every totally ordered subset admits an upper bound has a maximal element. We also proved an analogous version for preorders, where maximal is replaced with premaximal: t is premaximal if whenever t < s we also have s < t.

$| T | == T : Type is inhabited squash x == proof of $| T | (with x : T) unsquash s == extract a witness from s : $| T | > Tactic:

squash x: solves a goal $| T | by instantiating with x or [the T of x]

trivIset D F == the sets F i, where i ranges over D : set I, are pairwise-disjoint cover D F := \bigcup(i in D) F i partition D F A == the non-empty sets F i,where i ranges over D : set I, form a partition of A pblock_index D F x == index i such that i \in D and x \in F i pblock D F x := F (pblock_index D F x)

Upper and lower bounds:

ubound A == the set of upper bounds of the set A lbound A == the set of lower bounds of the set A Predicates to express existence conditions of supremum and infimum of sets of real numbers: has_ubound A := ubound A != set0 has_sup A := A != set0 /\ has_ubound A has_lbound A := lbound A != set0 has_inf A := A != set0 /\ has_lbound A

isLub A m := m is a least upper bound of the set A supremums A := set of supremums of the set A supremum x0 A == supremum of A or x0 if A is empty infimums A := set of infimums of the set A infimum x0 A == infimum of A or x0 if A is empty

F `#` G := the classes of sets F and G intersect

sections:

xsection A x == with A : set (T1 * T2) and x : T1 is the x-section of A ysection A y == with A : set (T1 * T2) and y : T2 is the y-section of A

About the naming conventions in this file:

use T, T', T1, T2, etc., aT (domain type), rT (return type) for names of variables in Type (or choiceType/pointedType/porderType) + use the same suffix or prefix for the sets as their containing type (e.g., A1 in T1, etc.) + as a consequence functions are rather of type aT -> rT
use I, J when the type corresponds to an index
sets are named A, B, C, D, etc., or Y when it is ostensibly an image set (i.e., of type set rT)
indexed sets are rather named F

Set Implicit Arguments.

Declare Scope classical_set_scope.

Reserved Notation "[ 'set' x : T | P ]"
  (at level 0, x at level 99, only parsing).
Reserved Notation "[ 'set' x | P ]"
  (at level 0, x, P at level 99, format "[ 'set' x | P ]").
Reserved Notation "[ 'set' E | x 'in' A ]" (at level 0, E, x at level 99,
  format "[ '[hv' 'set' E '/ ' | x 'in' A ] ']'").
Reserved Notation "[ 'set' E | x 'in' A & y 'in' B ]"
  (at level 0, E, x at level 99,
  format "[ '[hv' 'set' E '/ ' | x 'in' A & y 'in' B ] ']'").
Reserved Notation "[ 'set' a ]"
  (at level 0, a at level 99, format "[ 'set' a ]").
Reserved Notation "[ 'set' : T ]" (at level 0, format "[ 'set' : T ]").
Reserved Notation "[ 'set' a : T ]"
  (at level 0, a at level 99, format "[ 'set' a : T ]").
Reserved Notation "A `|` B" (at level 52, left associativity).
Reserved Notation "a |` A" (at level 52, left associativity).
Reserved Notation "[ 'set' a1 ; a2 ; .. ; an ]"
  (at level 0, a1 at level 99, format "[ 'set' a1 ; a2 ; .. ; an ]").
Reserved Notation "A `&` B" (at level 48, left associativity).
Reserved Notation "A `*` B" (at level 46, left associativity).
Reserved Notation "A `*`` B" (at level 46, left associativity).
Reserved Notation "A ``*` B" (at level 46, left associativity).
Reserved Notation "A .`1" (at level 2, left associativity, format "A .`1").
Reserved Notation "A .`2" (at level 2, left associativity, format "A .`2").
Reserved Notation "~` A" (at level 35, right associativity).
Reserved Notation "[ 'set' ~ a ]" (at level 0, format "[ 'set' ~ a ]").
Reserved Notation "A `\` B" (at level 50, left associativity).
Reserved Notation "A `\ b" (at level 50, left associativity).

Reserved Notation "A `+` B" (at level 54, left associativity). Reserved Notation "A +` B" (at level 54, left associativity).

Reserved Notation "\bigcup_ ( i 'in' P ) F"
  (at level 41, F at level 41, i, P at level 50,
           format "'[' \bigcup_ ( i 'in' P ) '/ ' F ']'").
Reserved Notation "\bigcup_ ( i : T ) F"
  (at level 41, F at level 41, i at level 50,
           format "'[' \bigcup_ ( i : T ) '/ ' F ']'").
Reserved Notation "\bigcup_ i F"
  (at level 41, F at level 41, i at level 0,
           format "'[' \bigcup_ i '/ ' F ']'").
Reserved Notation "\bigcap_ ( i 'in' P ) F"
  (at level 41, F at level 41, i, P at level 50,
           format "'[' \bigcap_ ( i 'in' P ) '/ ' F ']'").
Reserved Notation "\bigcap_ ( i : T ) F"
  (at level 41, F at level 41, i at level 50,
           format "'[' \bigcap_ ( i : T ) '/ ' F ']'").
Reserved Notation "\bigcap_ i F"
  (at level 41, F at level 41, i at level 0,
           format "'[' \bigcap_ i '/ ' F ']'").
Reserved Notation "A `<` B" (at level 70, no associativity).
Reserved Notation "A `<=` B" (at level 70, no associativity).
Reserved Notation "A `<=>` B" (at level 70, no associativity).
Reserved Notation "f @^-1` A" (at level 24).
Reserved Notation "f @` A" (at level 24).
Reserved Notation "A !=set0" (at level 80).
Reserved Notation "[ 'set`' p ]" (at level 0, format "[ 'set`' p ]").
Reserved Notation "[ 'disjoint' A & B ]" (at level 0,
  format "'[hv' [ 'disjoint' '/ ' A '/' & B ] ']'").
Reserved Notation "F `#` G"
(at level 48, left associativity, format "F `#` G").
Reserved Notation "'`I_' n" (at level 8, n at level 2, format "'`I_' n").

Definition set T := T → Prop.

we use fun x => instead of pred to prevent inE from working we will then extend inE with in_setE to make this work

Definition in_set T (A : set T) : pred T := (fun x ⇒ `[<A x >]).
Canonical set_predType T := @PredType T (set T) (@in_set T).

Lemma in_setE T (A : set T) x : x \in A = A x :> Prop.

Definition inE := (inE, in_setE ).

Bind Scope classical_set_scope with set.
Local Open Scope classical_set_scope.
Delimit Scope classical_set_scope with classic.

Definition mkset {T} (P : T → Prop) : set T := P.
Arguments mkset _ _ _ /.

Notation "[ 'set' x : T | P ]" := (mkset (fun x : T ⇒ P)) : classical_set_scope.
Notation "[ 'set' x | P ]" := [set x : _ | P] : classical_set_scope.

Definition image {T rT} (A : set T) (f : T → rT) :=
  [set y | exists2 x , A x & f x = y ].
Arguments image _ _ _ _ _ /.
Notation "[ 'set' E | x 'in' A ]" :=
  (image A (fun x ⇒ E)) : classical_set_scope.

Definition image2 {TA TB rT} (A : set TA) (B : set TB) (f : TA → TB → rT) :=
  [set z | exists2 x , A x & exists2 y , B y & f x y = z ].
Arguments image2 _ _ _ _ _ _ _ /.
Notation "[ 'set' E | x 'in' A & y 'in' B ]" :=
  (image2 A B (fun x y ⇒ E)) : classical_set_scope.

Section basic_definitions.
Context {T rT : Type}.
Implicit Types (T : Type) (A B : set T) (f : T → rT) (Y : set rT).

Definition preimage f Y : set T := [set t | Y (f t)].

Definition setT := [set _ : T | True ].
Definition set0 := [set _ : T | False ].
Definition set1 (t : T) := [set x : T | x = t ].
Definition setI A B := [set x | A x ∧ B x ].
Definition setU A B := [set x | A x ∨ B x ].
Definition nonempty A := ∃ a , A a.
Definition setC A := [set a | ¬ A a ].
Definition setD A B := [set x | A x ∧ ¬ B x ].
Definition setM T1 T2 (A1 : set T1) (A2 : set T2) := [set z | A1 z .1 ∧ A2 z .2 ].
Definition fst_set T1 T2 (A : set (T1 × T2)) := [set x | ∃ y , A (x , y )].
Definition snd_set T1 T2 (A : set (T1 × T2)) := [set y | ∃ x , A (x , y )].
Definition setMR T1 T2 (A1 : set T1) (A2 : T1 → set T2) :=
  [set z | A1 z .1 ∧ A2 z .1 z .2 ].
Definition setML T1 T2 (A1 : T2 → set T1) (A2 : set T2) :=
  [set z | A1 z .2 z .1 ∧ A2 z .2 ].

Lemma mksetE (P : T → Prop) x : [set x | P x ] x = P x.

Definition bigcap T I (P : set I) (F : I → set T) :=
  [set a | ∀ i, P i → F i a ].
Definition bigcup T I (P : set I) (F : I → set T) :=
  [set a | exists2 i , P i & F i a ].

Definition subset A B := ∀ t, A t → B t.

Definition disj_set A B := setI A B == set0.

Definition proper A B := A `<=` B ∧ ¬ (B `<=` A ).

End basic_definitions.
Arguments preimage T rT f Y t /.
Arguments set0 _ _ /.
Arguments setT _ _ /.
Arguments set1 _ _ _ /.
Arguments setI _ _ _ _ /.
Arguments setU _ _ _ _ /.
Arguments setC _ _ _ /.
Arguments setD _ _ _ _ /.
Arguments setM _ _ _ _ _ /.
Arguments setMR _ _ _ _ _ /.
Arguments setML _ _ _ _ _ /.
Arguments fst_set _ _ _ _ /.
Arguments snd_set _ _ _ _ /.

Notation range F := [set F i | i in setT ].
Notation "[ 'set' a ]" := (set1 a) : classical_set_scope.
Notation "[ 'set' a : T ]" := [set (a : T)] : classical_set_scope.
Notation "[ 'set' : T ]" := (@setT T) : classical_set_scope.
Notation "A `|` B" := (setU A B) : classical_set_scope.
Notation "a |` A" := ([set a] `|` A) : classical_set_scope.
Notation "[ 'set' a1 ; a2 ; .. ; an ]" :=
  (setU .. (a1 |` [set a2]) .. [set an]) : classical_set_scope.
Notation "A `&` B" := (setI A B) : classical_set_scope.
Notation "A `*` B" := (setM A B) : classical_set_scope.
Notation "A .`1" := (fst_set A) : classical_set_scope.
Notation "A .`2" := (snd_set A) : classical_set_scope.
Notation "A `*`` B" := (setMR A B) : classical_set_scope.
Notation "A ``*` B" := (setML A B) : classical_set_scope.
Notation "~` A" := (setC A) : classical_set_scope.
Notation "[ 'set' ~ a ]" := (~` [set a]) : classical_set_scope.
Notation "A `\` B" := (setD A B) : classical_set_scope.
Notation "A `\ a" := (A `\` [set a]) : classical_set_scope.
Notation "[ 'disjoint' A & B ]" := (disj_set A B) : classical_set_scope.

Notation "\bigcup_ ( i 'in' P ) F" :=
  (bigcup P (fun i ⇒ F)) : classical_set_scope.
Notation "\bigcup_ ( i : T ) F" :=
  (\bigcup_(i in @setT T) F) : classical_set_scope.
Notation "\bigcup_ i F" := (\bigcup_(i : _) F) : classical_set_scope.
Notation "\bigcap_ ( i 'in' P ) F" :=
  (bigcap P (fun i ⇒ F)) : classical_set_scope.
Notation "\bigcap_ ( i : T ) F" :=
  (\bigcap_(i in @setT T) F) : classical_set_scope.
Notation "\bigcap_ i F" := (\bigcap_(i : _) F) : classical_set_scope.

Notation "A `<=` B" := (subset A B) : classical_set_scope.
Notation "A `<` B" := (proper A B) : classical_set_scope.

Notation "A `<=>` B" := ((A `<=` B) ∧ (B `<=` A)) : classical_set_scope.
Notation "f @^-1` A" := (preimage f A) : classical_set_scope.
Notation "f @` A" := (image A f) (only parsing) : classical_set_scope.
Notation "A !=set0" := (nonempty A) : classical_set_scope.

Notation "[ 'set`' p ]":= [set x | is_true (x \in p)] : classical_set_scope.
Notation pred_set := (fun i ⇒ [set ` i ]).

Notation "`[ a , b ]" :=
  [set ` Interval (BLeft a) (BRight b)] : classical_set_scope.
Notation "`] a , b ]" :=
  [set ` Interval (BRight a) (BRight b)] : classical_set_scope.
Notation "`[ a , b [" :=
  [set ` Interval (BLeft a) (BLeft b)] : classical_set_scope.
Notation "`] a , b [" :=
  [set ` Interval (BRight a) (BLeft b)] : classical_set_scope.
Notation "`] '-oo' , b ]" :=
  [set ` Interval -oo%O (BRight b)] : classical_set_scope.
Notation "`] '-oo' , b [" :=
  [set ` Interval -oo%O (BLeft b)] : classical_set_scope.
Notation "`[ a , '+oo' [" :=
  [set ` Interval (BLeft a) +oo%O] : classical_set_scope.
Notation "`] a , '+oo' [" :=
  [set ` Interval (BRight a) +oo%O] : classical_set_scope.
Notation "`] -oo , '+oo' [" :=
  [set ` Interval -oo%O +oo%O] : classical_set_scope.

Lemma preimage_itv T (d : unit) (rT : porderType d) (f : T → rT) (i : interval rT) (x : T) :
  ((f @^-1` [set ` i ]) x ) = (f x \in i ).

Lemma preimage_itv_o_infty T (d : unit) (rT : porderType d) (f : T → rT) y :
  f @^-1` `]y , +oo [%classic = [set x | (y < f x)%O].

Lemma preimage_itv_c_infty T (d : unit) (rT : porderType d) (f : T → rT) y :
  f @^-1` `[y , +oo [%classic = [set x | (y ≤ f x)%O].

Lemma preimage_itv_infty_o T (d : unit) (rT : orderType d) (f : T → rT) y :
  f @^-1` `]-oo , y [%classic = [set x | (f x < y)%O].

Lemma preimage_itv_infty_c T (d : unit) (rT : orderType d) (f : T → rT) y :
  f @^-1` `]-oo , y ]%classic = [set x | (f x ≤ y)%O].

Notation "'`I_' n" := [set k | is_true (k < n)%N].

Lemma eq_set T (P Q : T → Prop) : (∀ x : T, P x = Q x ) →
  [set x | P x ] = [set x | Q x ].

Coercion set_type T (A : set T) := {x : T | x \in A }.

Definition SigSub {T} {pT : predType T} {P : pT} x : x \in P → {x | x \in P } :=
  exist (fun x ⇒ x \in P) x.

Lemma set0fun {P T : Type} : @set0 T → P.

Section basic_lemmas.
Context {T : Type}.
Implicit Types A B C D : set T.

Lemma mem_set {A} {u : T} : A u → u \in A.
Lemma set_mem {A} {u : T} : u \in A → A u.
Lemma mem_setT (u : T) : u \in [set : T ].
Lemma mem_setK {A} {u : T} : cancel (@mem_set A u) set_mem.
Lemma set_memK {A} {u : T} : cancel (@set_mem A u) mem_set.

Lemma memNset (A : set T) (u : T) : ¬ A u → u \in A = false.

Lemma notin_set (A : set T) x : (x \notin A : Prop ) = ¬ (A x ).

Lemma setTPn (A : set T) : A != setT ↔ ∃ t , ¬ A t.
#[deprecated(note="Use setTPn instead")]
Notation setTP := setTPn.

Lemma in_set0 (x : T) : (x \in set0 ) = false.
Lemma in_setT (x : T) : x \in setT.

Lemma in_setC (x : T) A : (x \in ~` A ) = (x \notin A ).

Lemma in_setI (x : T) A B : (x \in A `&` B ) = (x \in A ) && (x \in B ).

Lemma in_setD (x : T) A B : (x \in A `\` B ) = (x \in A ) && (x \notin B ).

Lemma in_setU (x : T) A B : (x \in A `|` B ) = (x \in A ) || (x \in B ).

Lemma in_setM T' (x : T × T') A E : (x \in A `*` E ) = (x .1 \in A ) && (x .2 \in E ).

Lemma set_valP {A} (x : A) : A (val x).

Lemma eqEsubset A B : (A = B ) = (A `<=>` B ).

Lemma seteqP A B : (A = B ) ↔ (A `<=>` B ).

Lemma set_true : [set ` predT ] = setT :> set T.

Lemma set_false : [set ` pred0 ] = set0 :> set T.

Lemma set_andb (P Q : {pred T }) : [set ` predI P Q ] = [set ` P ] `&` [set ` Q ].

Lemma set_orb (P Q : {pred T }) : [set ` predU P Q ] = [set ` P ] `|` [set ` Q ].

Lemma fun_true : (fun ⇒ true ) = setT :> set T.

Lemma fun_false : (fun ⇒ false ) = set0 :> set T.

Lemma set_mem_set A : [set ` A ] = A.

Lemma mem_setE (P : pred T) : mem [set ` P ] = mem P.

Lemma subset_refl A : A `<=` A.

Lemma subset_trans B A C : A `<=` B → B `<=` C → A `<=` C.

Lemma sub0set A : set0 `<=` A.

Lemma setC0 : ~` set0 = setT :> set T.

Lemma setCK : involutive (@setC T).

Lemma setCT : ~` setT = set0 :> set T.

Definition setC_inj := can_inj setCK.

Lemma setIC : commutative (@setI T).

Lemma setIS C A B : A `<=` B → C `&` A `<=` C `&` B.

Lemma setSI C A B : A `<=` B → A `&` C `<=` B `&` C.

Lemma setISS A B C D : A `<=` C → B `<=` D → A `&` B `<=` C `&` D.

Lemma setIT : right_id setT (@setI T).

Lemma setTI : left_id setT (@setI T).

Lemma setI0 : right_zero set0 (@setI T).

Lemma set0I : left_zero set0 (@setI T).

Lemma setICl : left_inverse set0 setC (@setI T).

Lemma setICr : right_inverse set0 setC (@setI T).

Lemma setIA : associative (@setI T).

Lemma setICA : left_commutative (@setI T).

Lemma setIAC : right_commutative (@setI T).

Lemma setIACA : @interchange (set T) setI setI.

Lemma setIid : idempotent (@setI T).

Lemma setIIl A B C : A `&` B `&` C = (A `&` C ) `&` (B `&` C ).

Lemma setIIr A B C : A `&` (B `&` C ) = (A `&` B ) `&` (A `&` C ).

Lemma setUC : commutative (@setU T).

Lemma setUS C A B : A `<=` B → C `|` A `<=` C `|` B.

Lemma setSU C A B : A `<=` B → A `|` C `<=` B `|` C.

Lemma setUSS A B C D : A `<=` C → B `<=` D → A `|` B `<=` C `|` D.

Lemma setTU : left_zero setT (@setU T).

Lemma setUT : right_zero setT (@setU T).

Lemma set0U : left_id set0 (@setU T).

Lemma setU0 : right_id set0 (@setU T).

Lemma setUCl : left_inverse setT setC (@setU T).

Lemma setUCr : right_inverse setT setC (@setU T).

Lemma setUA : associative (@setU T).

Lemma setUCA : left_commutative (@setU T).

Lemma setUAC : right_commutative (@setU T).

Lemma setUACA : @interchange (set T) setU setU.

Lemma setUid : idempotent (@setU T).

Lemma setUUl A B C : A `|` B `|` C = (A `|` C ) `|` (B `|` C ).

Lemma setUUr A B C : A `|` (B `|` C ) = (A `|` B ) `|` (A `|` C ).

Lemma setDE A B : A `\` B = A `&` ~` B.

Lemma setDUK A B : A `<=` B → A `|` (B `\` A ) = B.

Lemma setDKU A B : A `<=` B → (B `\` A ) `|` A = B.

Lemma setDv A : A `\` A = set0.

Lemma setUv A : A `|` ~` A = setT.

Lemma setIv A : A `&` ~` A = set0.
Lemma setvU A : ~` A `|` A = setT.
Lemma setvI A : ~` A `&` A = set0.

Lemma setUCK A B : (A `|` B ) `|` ~` B = setT.

Lemma setUKC A B : ~` A `|` (A `|` B ) = setT.

Lemma setICK A B : (A `&` B ) `&` ~` B = set0.

Lemma setIKC A B : ~` A `&` (A `&` B ) = set0.

Lemma setDIK A B : A `&` (B `\` A ) = set0.

Lemma setDKI A B : (B `\` A ) `&` A = set0.

Lemma setD1K a A : A a → a |` A `\ a = A.

Lemma setI1 A a : A `&` [set a ] = if a \in A then [set a ] else set0.

Lemma set1I A a : [set a ] `&` A = if a \in A then [set a ] else set0.

Lemma subset0 A : (A `<=` set0 ) = (A = set0 ).

Lemma subTset A : (setT `<=` A ) = (A = setT ).

Lemma subsetT A : A `<=` setT.

Lemma subsetW {A B} : A = B → A `<=` B.

Definition subsetCW {A B} : A = B → B `<=` A := subsetW \o esym.

Lemma disj_set2E A B : [disjoint A & B ] = (A `&` B == set0 ).

Lemma disj_set2P {A B} : reflect (A `&` B = set0) [disjoint A & B ]%classic.

Lemma disj_setPS {A B} : reflect (A `&` B `<=` set0) [disjoint A & B ]%classic.

Lemma disj_set_sym A B : [disjoint B & A ] = [disjoint A & B ].

Lemma disj_setPCl {A B} : reflect (A `<=` B) [disjoint A & ~` B ]%classic.

Lemma disj_setPCr {A B} : reflect (A `<=` B) [disjoint ~` B & A ]%classic.

Lemma disj_setPLR {A B} : reflect (A `<=` ~` B) [disjoint A & B ]%classic.

Lemma disj_setPRL {A B} : reflect (B `<=` ~` A) [disjoint A & B ]%classic.

Lemma subsets_disjoint A B : A `<=` B ↔ A `&` ~` B = set0.

Lemma disjoints_subset A B : A `&` B = set0 ↔ A `<=` ~` B.

Lemma subsetC1 x A : (A `<=` [set ¬ x ]) = (x \in ~` A ).

Lemma setSD C A B : A `<=` B → A `\` C `<=` B `\` C.

Lemma setTD A : setT `\` A = ~` A.

Lemma set0P A : (A != set0 ) ↔ (A !=set0 ).

Lemma setF_eq0 : (T → False ) → all_equal_to (set0 : set T).

Lemma subset_nonempty A B : A `<=` B → A !=set0 → B !=set0.

Lemma subsetC A B : A `<=` B → ~` B `<=` ~` A.

Lemma subsetCl A B : ~` A `<=` B → ~` B `<=` A.

Lemma subsetCr A B : A `<=` ~` B → B `<=` ~` A.

Lemma subsetC2 A B : ~` A `<=` ~` B → B `<=` A.

Lemma subsetCP A B : ~` A `<=` ~` B ↔ B `<=` A.

Lemma subsetCPl A B : ~` A `<=` B ↔ ~` B `<=` A.

Lemma subsetCPr A B : A `<=` ~` B ↔ B `<=` ~` A.

Lemma subsetUl A B : A `<=` A `|` B.

Lemma subsetUr A B : B `<=` A `|` B.

Lemma subUset A B C : (B `|` C `<=` A ) = ((B `<=` A ) ∧ (C `<=` A )).

Lemma setIidPl A B : A `&` B = A ↔ A `<=` B.

Lemma setIidPr A B : A `&` B = B ↔ B `<=` A.

Lemma setIidl A B : A `<=` B → A `&` B = A.
Lemma setIidr A B : B `<=` A → A `&` B = B.

Lemma setUidPl A B : A `|` B = A ↔ B `<=` A.

Lemma setUidPr A B : A `|` B = B ↔ A `<=` B.

Lemma setUidl A B : B `<=` A → A `|` B = A.
Lemma setUidr A B : A `<=` B → A `|` B = B.

Lemma subsetI A B C : (A `<=` B `&` C ) = ((A `<=` B ) ∧ (A `<=` C )).

Lemma setDidPl A B : A `\` B = A ↔ A `&` B = set0.

Lemma setDidl A B : A `&` B = set0 → A `\` B = A.

Lemma subIset A B C : A `<=` C ∨ B `<=` C → A `&` B `<=` C.

Lemma subIsetl A B : A `&` B `<=` A.

Lemma subIsetr A B : A `&` B `<=` B.

Lemma subDsetl A B : A `\` B `<=` A.

Lemma subDsetr A B : A `\` B `<=` ~` B.

Lemma subsetI_neq0 A B C D :
  A `<=` B → C `<=` D → A `&` C !=set0 → B `&` D !=set0.

Lemma subsetI_eq0 A B C D :
  A `<=` B → C `<=` D → B `&` D = set0 → A `&` C = set0.

Lemma setD_eq0 A B : (A `\` B = set0 ) = (A `<=` B ).

Lemma properEneq A B : (A `<` B ) = (A != B ∧ A `<=` B ).

Lemma nonsubset A B : ¬ (A `<=` B ) → A `&` ~` B !=set0.

Lemma setU_eq0 A B : (A `|` B = set0 ) = ((A = set0 ) ∧ (B = set0 )).

Lemma setCS A B : (~` A `<=` ~` B ) = (B `<=` A ).

Lemma setDT A : A `\` setT = set0.

Lemma set0D A : set0 `\` A = set0.

Lemma setD0 A : A `\` set0 = A.

Lemma setDS C A B : A `<=` B → C `\` B `<=` C `\` A.

Lemma setDSS A B C D : A `<=` C → D `<=` B → A `\` B `<=` C `\` D.

Lemma setCU A B : ~`(A `|` B ) = ~` A `&` ~` B.

Lemma setCI A B : ~` (A `&` B ) = ~` A `|` ~` B.

Lemma setDUr A B C : A `\` (B `|` C ) = (A `\` B ) `&` (A `\` C ).

Lemma setIUl : left_distributive (@setI T) (@setU T).

Lemma setIUr : right_distributive (@setI T) (@setU T).

Lemma setUIl : left_distributive (@setU T) (@setI T).

Lemma setUIr : right_distributive (@setU T) (@setI T).

Lemma setUK A B : (A `|` B ) `&` A = A.

Lemma setKU A B : A `&` (B `|` A ) = A.

Lemma setIK A B : (A `&` B ) `|` A = A.

Lemma setKI A B : A `|` (B `&` A ) = A.

Lemma setDUl : left_distributive setD (@setU T).

Lemma setUKD A B : A `&` B `<=` set0 → (A `|` B ) `\` A = B.

Lemma setUDK A B : A `&` B `<=` set0 → (B `|` A ) `\` A = B.

Lemma setIDA A B C : A `&` (B `\` C ) = (A `&` B ) `\` C.

Lemma setDD A B : A `\` (A `\` B ) = A `&` B.

Lemma setDDl A B C : (A `\` B ) `\` C = A `\` (B `|` C ).

Lemma setDDr A B C : A `\` (B `\` C ) = (A `\` B ) `|` (A `&` C ).

Lemma setDIr A B C : A `\` B `&` C = (A `\` B ) `|` (A `\` C ).

Lemma setUIDK A B : (A `&` B ) `|` A `\` B = A.

Lemma setM0 T' (A : set T) : A `*` set0 = set0 :> set (T × T').

Lemma set0M T' (A : set T') : set0 `*` A = set0 :> set (T × T').

Lemma setMTT T' : setT `*` setT = setT :> set (T × T').

Lemma setMT T1 T2 (A : set T1) : A `*` @setT T2 = fst @^-1` A.

Lemma setTM T1 T2 (B : set T2) : @setT T1 `*` B = snd @^-1` B.

Lemma setMI T1 T2 (X1 : set T1) (X2 : set T2) (Y1 : set T1) (Y2 : set T2) :
  (X1 `&` Y1 ) `*` (X2 `&` Y2 ) = X1 `*` X2 `&` Y1 `*` Y2.

Lemma setSM T1 T2 (C D : set T1) (A B : set T2) :
  A `<=` B → C `<=` D → C `*` A `<=` D `*` B.

Lemma setM_bigcupr T1 T2 I (F : I → set T2) (P : set I) (A : set T1) :
  A `*` \bigcup_(i in P ) F i = \bigcup_(i in P ) (A `*` F i ).

Lemma setM_bigcupl T1 T2 I (F : I → set T2) (P : set I) (A : set T1) :
  \bigcup_(i in P ) F i `*` A = \bigcup_(i in P ) (F i `*` A ).

Lemma bigcupM1l T1 T2 (A1 : set T1) (A2 : T1 → set T2) :
  \bigcup_(i in A1 ) ([set i ] `*` (A2 i )) = A1 `*`` A2.

Lemma bigcupM1r T1 T2 (A1 : T2 → set T1) (A2 : set T2) :
  \bigcup_(i in A2 ) (A1 i `*` [set i ]) = A1 ``*` A2.

Lemma pred_oappE (D : {pred T }) : pred_oapp D = mem (some @` D).

Lemma pred_oapp_set (D : set T) : pred_oapp (mem D) = mem (some @` D).

End basic_lemmas.
#[global]
Hint Resolve subsetUl subsetUr subIsetl subIsetr subDsetl subDsetr : core.

Lemma image2E {TA TB rT : Type} (A : set TA) (B : set TB) (f : TA → TB → rT) :
  [set f x y | x in A & y in B ] = uncurry f @` (A `*` B ).

Lemma set_nil (T : choiceType) : [set ` [::]] = @set0 T.

Lemma set_seq_eq0 (T : eqType) (S : seq T) : ([set ` S ] == set0 ) = (S == [::]).

Lemma set_fset_eq0 (T : choiceType) (S : {fset T}) :
  ([set ` S ] == set0 ) = (S == fset0).

Section InitialSegment.

Lemma II0 : `I_0 = set0.

Lemma II1 : `I_1 = [set 0%N].

Lemma IIn_eq0 n : `I_n = set0 → n = 0%N.

Lemma IIS n : `I_n.+1 = `I_n `|` [set n ].

Lemma setI_II m n : `I_m `&` `I_n = `I_(minn m n ).

Lemma setU_II m n : `I_m `|` `I_n = `I_(maxn m n ).

Lemma Iiota (n : nat) : [set ` iota 0 n ] = `I_n.

Definition ordII {n} (k : 'I_n) : `I_n := SigSub (@mem_set _ `I_n _ (ltn_ord k)).
Definition IIord {n} (k : `I_n) := Ordinal (set_valP k).

Definition ordIIK {n} : cancel (@ordII n) IIord.

Lemma IIordK {n} : cancel (@IIord n) ordII.

End InitialSegment.

Lemma setT_unit : [set : unit ] = [set tt ].

Lemma setT_bool : [set : bool ] = [set true ; false ].

TODO: other lemmas that relate fset and classical sets

Lemma fdisjoint_cset (T : choiceType) (A B : {fset T}) :
  [disjoint A & B]%fset = [disjoint [set ` A ] & [set ` B ]].

Section SetFset.
Context {T : choiceType}.
Implicit Types (x y : T) (A B : {fset T}).

Lemma set_fset0 : [set y : T | y \in fset0] = set0.

Lemma set_fset1 x : [set y | y \in [fset x]%fset] = [set x ].

Lemma set_fsetI A B : [set ` (A `&` B)%fset] = [set ` A ] `&` [set ` B ].

Lemma set_fsetIr (P : {pred T }) (A : {fset T}) :
  [set ` [fset x | x in A & P x]%fset] = [set ` A ] `&` [set ` P ].

Lemma set_fsetU A B :
  [set ` (A `|` B)%fset] = [set ` A ] `|` [set ` B ].

Lemma set_fsetU1 x A : [set y | y \in (x |` A)%fset] = x |` [set ` A ].

Lemma set_fsetD A B :
  [set ` (A `\` B)%fset] = [set ` A ] `\` [set ` B ].

Lemma set_fsetD1 A x : [set y | y \in (A `\ x)%fset] = [set ` A ] `\ x.

Lemma set_imfset (key : unit) [K : choiceType] (f : T → K) (p : finmempred T) :
  [set ` imfset key f p ] = f @` [set ` p ].

End SetFset.

Section SetMonoids.
Variable (T : Type).

Import Monoid.
Canonical setU_monoid := Law (@setUA T) (@set0U T) (@setU0 T).
Canonical setU_comoid := ComLaw (@setUC T).
Canonical setU_mul_monoid := MulLaw (@setTU T) (@setUT T).
Canonical setI_monoid := Law (@setIA T) (@setTI T) (@setIT T).
Canonical setI_comoid := ComLaw (@setIC T).
Canonical setI_mul_monoid := MulLaw (@set0I T) (@setI0 T).
Canonical setU_add_monoid := AddLaw (@setUIl T) (@setUIr T).
Canonical setI_add_monoid := AddLaw (@setIUl T) (@setIUr T).

End SetMonoids.

Section base_image_lemmas.
Context {aT rT : Type}.
Implicit Types (A B : set aT) (f : aT → rT) (Y : set rT).

Lemma imageP f A a : A a → (f @` A ) (f a ).

Lemma imageT (f : aT → rT) (a : aT) : range f (f a).

End base_image_lemmas.
#[global]
Hint Extern 0 ((?f @` _) (?f _)) ⇒ solve [apply: imageP; assumption] : core.
#[global] Hint Extern 0 ((?f @` setT ) _) ⇒ solve [apply: imageT] : core.

Section image_lemmas.
Context {aT rT : Type}.
Implicit Types (A B : set aT) (f : aT → rT) (Y : set rT).

Lemma image_inj {f A a} : injective f → (f @` A ) (f a ) = A a.

Lemma image_id A : id @` A = A.

Lemma homo_setP {A Y f} :
  {homo f : x / x \in A >-> x \in Y } ↔ {homo f : x / A x >-> Y x }.

Lemma image_subP {A Y f} : f @` A `<=` Y ↔ {homo f : x / A x >-> Y x }.

Lemma image_sub {f : aT → rT} {A : set aT} {B : set rT} :
  (f @` A `<=` B ) = (A `<=` f @^-1` B ).

Lemma image_setU f A B : f @` (A `|` B ) = f @` A `|` f @` B.

Lemma image_set0 f : f @` set0 = set0.

Lemma image_set0_set0 A f : f @` A = set0 → A = set0.

Lemma image_set1 f t : f @` [set t ] = [set f t ].

Lemma subset_set1 A a : A `<=` [set a ] → A = set0 ∨ A = [set a ].

Lemma subset_set2 A a b : A `<=` [set a ; b ] →
  [\/ A = set0 , A = [set a ], A = [set b ] | A = [set a ; b ]].

Lemma sub_image_setI f A B : f @` (A `&` B ) `<=` f @` A `&` f @` B.

Lemma nonempty_image f A : f @` A !=set0 → A !=set0.

Lemma image_subset f A B : A `<=` B → f @` A `<=` f @` B.

Lemma preimage_set0 f : f @^-1` set0 = set0.

Lemma preimage_setT f : f @^-1` setT = setT.

Lemma nonempty_preimage f Y : f @^-1` Y !=set0 → Y !=set0.

Lemma preimage_image f A : A `<=` f @^-1` (f @` A ).

Lemma image_preimage_subset f Y : f @` (f @^-1` Y ) `<=` Y.

Lemma image_preimage f Y : f @` setT = setT → f @` (f @^-1` Y ) = Y.

Lemma eq_imagel T1 T2 (A : set T1) (f f' : T1 → T2) :
  (∀ x, A x → f x = f' x ) → f @` A = f' @` A.

Lemma preimage_setU f Y1 Y2 : f @^-1` (Y1 `|` Y2 ) = f @^-1` Y1 `|` f @^-1` Y2.

Lemma preimage_setI f Y1 Y2 : f @^-1` (Y1 `&` Y2 ) = f @^-1` Y1 `&` f @^-1` Y2.

Lemma preimage_setC f Y : ~` (f @^-1` Y ) = f @^-1` (~` Y ).

Lemma preimage_subset f Y1 Y2 : Y1 `<=` Y2 → f @^-1` Y1 `<=` f @^-1` Y2.

Lemma nonempty_preimage_setI f Y1 Y2 :
  (f @^-1` (Y1 `&` Y2 )) !=set0 ↔ (f @^-1` Y1 `&` f @^-1` Y2 ) !=set0.

Lemma preimage_bigcup {I} (P : set I) f (F : I → set rT) :
  f @^-1` (\bigcup_ (i in P ) F i ) = \bigcup_(i in P ) (f @^-1` F i ).

Lemma preimage_bigcap {I} (P : set I) f (F : I → set rT) :
  f @^-1` (\bigcap_ (i in P ) F i ) = \bigcap_(i in P ) (f @^-1` F i ).

Lemma eq_preimage {I T : Type} (D : set I) (A : set T) (F G : I → T) :
  {in D , F =1 G } → D `&` F @^-1` A = D `&` G @^-1` A.

Lemma notin_setI_preimage T R D (f : T → R) i :
  i \notin f @` D → D `&` f @^-1` [set i ] = set0.

Lemma comp_preimage T1 T2 T3 (A : set T3) (g : T1 → T2) (f : T2 → T3) :
  (f \o g ) @^-1` A = g @^-1` (f @^-1` A ).

Lemma preimage_id T (A : set T) : id @^-1` A = A.

Lemma preimage_comp T1 T2 (g : T1 → rT) (f : T2 → rT) (C : set T1) :
  f @^-1` [set g x | x in C ] = [set x | f x \in g @` C ].

Lemma preimage_setI_eq0 (f : aT → rT) (Y1 Y2 : set rT) :
  f @^-1` (Y1 `&` Y2 ) = set0 ↔ f @^-1` Y1 `&` f @^-1` Y2 = set0.

Lemma preimage0eq (f : aT → rT) (Y : set rT) : Y = set0 → f @^-1` Y = set0.

Lemma preimage0 {T R} {f : T → R} {A : set R} :
  A `&` range f `<=` set0 → f @^-1` A = set0.

Lemma preimage10P {T R} {f : T → R} {x} : ¬ range f x ↔ f @^-1` [set x ] = set0.

Lemma preimage10 {T R} {f : T → R} {x} : ¬ range f x → f @^-1` [set x ] = set0.

End image_lemmas.
Arguments sub_image_setI {aT rT f A B} t _.

Lemma image_comp T1 T2 T3 (f : T1 → T2) (g : T2 → T3) A :
  g @` (f @` A ) = (g \o f ) @` A.

Lemma some_set0 {T} : some @` set0 = set0 :> set (option T).

Lemma some_set1 {T} (x : T) : some @` [set x ] = [set some x ].

Lemma some_setC {T} (A : set T) : some @` (~` A ) = [set ¬ None ] `\` (some @` A ).

Lemma some_setT {T} : some @` [set : T ] = [set ¬ None ].

Lemma some_setI {T} (A B : set T) : some @` (A `&` B ) = some @` A `&` some @` B.

Lemma some_setU {T} (A B : set T) : some @` (A `|` B ) = some @` A `|` some @` B.

Lemma some_setD {T} (A B : set T) : some @` (A `\` B ) = (some @` A ) `\` (some @` B ).

Lemma sub_image_some {T} (A B : set T) : some @` A `<=` some @` B → A `<=` B.

Lemma sub_image_someP {T} (A B : set T) : some @` A `<=` some @` B ↔ A `<=` B.

Lemma image_some_inj {T} (A B : set T) : some @` A = some @` B → A = B.

Lemma some_set_eq0 {T} (A : set T) : some @` A = set0 ↔ A = set0.

Lemma some_preimage {aT rT} (f : aT → rT) (A : set rT) :
  some @` (f @^-1` A ) = omap f @^-1` (some @` A ).

Lemma some_image {aT rT} (f : aT → rT) (A : set aT) :
  some @` (f @` A ) = omap f @` (some @` A ).

Lemma disj_set_some {T} {A B : set T} :
  [disjoint some @` A & some @` B ] = [disjoint A & B ].

Section bigop_lemmas.
Context {T I : Type}.
Implicit Types (A : set T) (i : I) (P : set I) (F G : I → set T).

Lemma bigcup_sup i P F : P i → F i `<=` \bigcup_(j in P ) F j.

Lemma bigcap_inf i P F : P i → \bigcap_(j in P ) F j `<=` F i.

Lemma subset_bigcup_r P : {homo (fun x : I → set T ⇒ \bigcup_(i in P ) x i )
  : F G / [set F i | i in P ] `<=` [set G i | i in P ] >-> F `<=` G }.

Lemma subset_bigcap_r P : {homo (fun x : I → set T ⇒ \bigcap_(i in P ) x i )
  : F G / [set F i | i in P ] `<=` [set G i | i in P ] >-> G `<=` F }.

Lemma eq_bigcupr P F G : (∀ i, P i → F i = G i ) →
  \bigcup_(i in P ) F i = \bigcup_(i in P ) G i.

Lemma eq_bigcapr P F G : (∀ i, P i → F i = G i ) →
  \bigcap_(i in P ) F i = \bigcap_(i in P ) G i.

Lemma setC_bigcup P F : ~` (\bigcup_(i in P ) F i ) = \bigcap_(i in P ) ~` F i.

Lemma setC_bigcap P F : ~` (\bigcap_(i in P ) (F i )) = \bigcup_(i in P ) ~` F i.

Lemma image_bigcup rT P F (f : T → rT) :
  f @` (\bigcup_(i in P ) (F i )) = \bigcup_(i in P ) f @` F i.

Lemma some_bigcap P F : some @` (\bigcap_(i in P ) (F i )) =
  [set ¬ None ] `&` \bigcap_(i in P ) some @` F i.

Lemma bigcup_set_type P F : \bigcup_(i in P ) F i = \bigcup_(j : P ) F (val j).

Lemma eq_bigcupl P Q F : P `<=>` Q →
  \bigcup_(i in P ) F i = \bigcup_(i in Q ) F i.

Lemma eq_bigcapl P Q F : P `<=>` Q →
  \bigcap_(i in P ) F i = \bigcap_(i in Q ) F i.

Lemma eq_bigcup P Q F G : P `<=>` Q → (∀ i, P i → F i = G i ) →
  \bigcup_(i in P ) F i = \bigcup_(i in Q ) G i.

Lemma eq_bigcap P Q F G : P `<=>` Q → (∀ i, P i → F i = G i ) →
  \bigcap_(i in P ) F i = \bigcap_(i in Q ) G i.

Lemma bigcupU P F G : \bigcup_(i in P ) (F i `|` G i ) =
  (\bigcup_(i in P ) F i ) `|` (\bigcup_(i in P ) G i ).

Lemma bigcapI P F G : \bigcap_(i in P ) (F i `&` G i ) =
  (\bigcap_(i in P ) F i ) `&` (\bigcap_(i in P ) G i ).

Lemma bigcup_const P A : P !=set0 → \bigcup_(_ in P ) A = A.

Lemma bigcap_const P A : P !=set0 → \bigcap_(_ in P ) A = A.

Lemma bigcapIl P F A : P !=set0 →
  \bigcap_(i in P ) (F i `&` A ) = \bigcap_(i in P ) F i `&` A.

Lemma bigcapIr P F A : P !=set0 →
  \bigcap_(i in P ) (A `&` F i ) = A `&` \bigcap_(i in P ) F i.

Lemma bigcupUl P F A : P !=set0 →
  \bigcup_(i in P ) (F i `|` A ) = \bigcup_(i in P ) F i `|` A.

Lemma bigcupUr P F A : P !=set0 →
  \bigcup_(i in P ) (A `|` F i ) = A `|` \bigcup_(i in P ) F i.

Lemma bigcup_set0 F : \bigcup_(i in set0 ) F i = set0.

Lemma bigcup_set1 F i : \bigcup_(j in [set i ]) F j = F i.

Lemma bigcap_set0 F : \bigcap_(i in set0 ) F i = setT.

Lemma bigcap_set1 F i : \bigcap_(j in [set i ]) F j = F i.

Lemma bigcup_nonempty P F :
  (\bigcup_(i in P ) F i !=set0 ) ↔ exists2 i , P i & F i !=set0.

Lemma bigcup0 P F :
  (∀ i, P i → F i = set0 ) → \bigcup_(i in P ) F i = set0.

Lemma bigcap0 P F :
  (exists2 i , P i & F i = set0 ) → \bigcap_(i in P ) F i = set0.

Lemma bigcapT P F :
  (∀ i, P i → F i = setT ) → \bigcap_(i in P ) F i = setT.

Lemma bigcupT P F :
  (exists2 i , P i & F i = setT ) → \bigcup_(i in P ) F i = setT.

Lemma bigcup0P P F :
  (\bigcup_(i in P ) F i = set0 ) ↔ ∀ i, P i → F i = set0.

Lemma bigcapTP P F :
  (\bigcap_(i in P ) F i = setT ) ↔ ∀ i, P i → F i = setT.

Lemma setI_bigcupr F P A :
  A `&` \bigcup_(i in P ) F i = \bigcup_(i in P ) (A `&` F i ).

Lemma setI_bigcupl F P A :
  \bigcup_(i in P ) F i `&` A = \bigcup_(i in P ) (F i `&` A ).

Lemma setU_bigcapr F P A :
  A `|` \bigcap_(i in P ) F i = \bigcap_(i in P ) (A `|` F i ).

Lemma setU_bigcapl F P A :
  \bigcap_(i in P ) F i `|` A = \bigcap_(i in P ) (F i `|` A ).

Lemma bigcup_mkcond P F :
  \bigcup_(i in P ) F i = \bigcup_i if i \in P then F i else set0.

Lemma bigcup_mkcondr P Q F :
  \bigcup_(i in P `&` Q ) F i = \bigcup_(i in P ) if i \in Q then F i else set0.

Lemma bigcup_mkcondl P Q F :
  \bigcup_(i in P `&` Q ) F i = \bigcup_(i in Q ) if i \in P then F i else set0.

Lemma bigcap_mkcond F P :
  \bigcap_(i in P ) F i = \bigcap_i if i \in P then F i else setT.

Lemma bigcap_mkcondr P Q F :
  \bigcap_(i in P `&` Q ) F i = \bigcap_(i in P ) if i \in Q then F i else setT.

Lemma bigcap_mkcondl P Q F :
  \bigcap_(i in P `&` Q ) F i = \bigcap_(i in Q ) if i \in P then F i else setT.

Lemma bigcup_imset1 P (f : I → T) : \bigcup_(x in P ) [set f x ] = f @` P.

Lemma bigcup_setU F (X Y : set I) :
  \bigcup_(i in X `|` Y ) F i = \bigcup_(i in X ) F i `|` \bigcup_(i in Y ) F i.

Lemma bigcap_setU F (X Y : set I) :
  \bigcap_(i in X `|` Y ) F i = \bigcap_(i in X ) F i `&` \bigcap_(i in Y ) F i.

Lemma bigcup_setU1 F (x : I) (X : set I) :
  \bigcup_(i in x |` X ) F i = F x `|` \bigcup_(i in X ) F i.

Lemma bigcap_setU1 F (x : I) (X : set I) :
  \bigcap_(i in x |` X ) F i = F x `&` \bigcap_(i in X ) F i.

Lemma bigcup_setD1 (x : I) F (X : set I) : X x →
  \bigcup_(i in X ) F i = F x `|` \bigcup_(i in X `\ x ) F i.

Lemma bigcap_setD1 (x : I) F (X : set I) : X x →
  \bigcap_(i in X ) F i = F x `&` \bigcap_(i in X `\ x ) F i.

Lemma setC_bigsetU U (s : seq T) (f : T → set U) (P : pred T) :
   (~` \big[setU/set0]_(t <- s | P t) f t ) = \big[setI/setT]_(t <- s | P t) ~` f t.

Lemma setC_bigsetI U (s : seq T) (f : T → set U) (P : pred T) :
   (~` \big[setI/setT]_(t <- s | P t) f t ) = \big[setU/set0]_(t <- s | P t) ~` f t.

Lemma bigcupDr (F : I → set T) (P : set I) (A : set T) : P !=set0 →
  \bigcap_(i in P ) (A `\` F i ) = A `\` \bigcup_(i in P ) F i.

Lemma setD_bigcupl (F : I → set T) (P : set I) (A : set T) :
  \bigcup_(i in P ) F i `\` A = \bigcup_(i in P ) (F i `\` A ).

Lemma bigcup_bigcup_dep {J : Type} (F : I → J → set T) (P : set I) (Q : I → set J) :
  \bigcup_(i in P ) \bigcup_(j in Q i ) F i j =
  \bigcup_(k in P `*`` Q ) F k .1 k .2.

Lemma bigcup_bigcup {J : Type} (F : I → J → set T) (P : set I) (Q : set J) :
  \bigcup_(i in P ) \bigcup_(j in Q ) F i j =
  \bigcup_(k in P `*` Q ) F k .1 k .2.

Lemma bigcupID (Q : set I) (F : I → set T) (P : set I) :
  \bigcup_(i in P ) F i =
    (\bigcup_(i in P `&` Q ) F i ) `|` (\bigcup_(i in P `&` ~` Q ) F i ).

Lemma bigcapID (Q : set I) (F : I → set T) (P : set I) :
  \bigcap_(i in P ) F i =
    (\bigcap_(i in P `&` Q ) F i ) `&` (\bigcap_(i in P `&` ~` Q ) F i ).

End bigop_lemmas.
Arguments bigcup_setD1 {T I} x.
Arguments bigcap_setD1 {T I} x.

Definition bigcup2 T (A B : set T) : nat → set T :=
  fun i ⇒ if i == 0%N then A else if i == 1%N then B else set0.
Arguments bigcup2 T A B n /.

Lemma bigcup2E T (A B : set T) : \bigcup_i (bigcup2 A B) i = A `|` B.

Lemma bigcup2inE T (A B : set T) : \bigcup_(i in `I_2 ) (bigcup2 A B) i = A `|` B.

Definition bigcap2 T (A B : set T) : nat → set T :=
  fun i ⇒ if i == 0%N then A else if i == 1%N then B else setT.
Arguments bigcap2 T A B n /.

Lemma bigcap2E T (A B : set T) : \bigcap_i (bigcap2 A B) i = A `&` B.

Lemma bigcap2inE T (A B : set T) : \bigcap_(i in `I_2 ) (bigcap2 A B) i = A `&` B.

Lemma bigcup_sub T I (F : I → set T) (D : set T) (P : set I) :
  (∀ i, P i → F i `<=` D ) → \bigcup_(i in P ) F i `<=` D.

Lemma sub_bigcap T I (F : I → set T) (D : set T) (P : set I) :
  (∀ i, P i → D `<=` F i ) → D `<=` \bigcap_(i in P ) F i.

Lemma subset_bigcup T I [P : set I] [F G : I → set T] :
  (∀ i, P i → F i `<=` G i ) →
  \bigcup_(i in P ) F i `<=` \bigcup_(i in P ) G i.

Lemma subset_bigcap T I [P : set I] [F G : I → set T] :
  (∀ i, P i → F i `<=` G i ) →
  \bigcap_(i in P ) F i `<=` \bigcap_(i in P ) G i.

Lemma bigcup_image {aT rT I} (P : set aT) (f : aT → I) (F : I → set rT) :
  \bigcup_(x in f @` P ) F x = \bigcup_(x in P ) F (f x).

Lemma bigcap_set_type {I T} (P : set I) (F : I → set T) :
   \bigcap_(i in P ) F i = \bigcap_(j : P ) F (val j).

Lemma bigcap_image {aT rT I} (P : set aT) (f : aT → I) (F : I → set rT) :
  \bigcap_(x in f @` P ) F x = \bigcap_(x in P ) F (f x).

Lemma bigcup_fset {I : choiceType} {U : Type}
    (F : I → set U) (X : {fset I}) :
  \bigcup_(i in [set i | i \in X ]) F i = \big[setU/set0]_(i <- X) F i :> set U.

Lemma bigcap_fset {I : choiceType} {U : Type}
    (F : I → set U) (X : {fset I}) :
  \bigcap_(i in [set i | i \in X ]) F i = \big[setI/setT]_(i <- X) F i :> set U.

Lemma bigcup_fsetU1 {T U : choiceType} (F : T → set U) (x : T) (X : {fset T}) :
  \bigcup_(i in [set j | j \in x |` X ]%fset) F i =
  F x `|` \bigcup_(i in [set j | j \in X ]) F i.

Lemma bigcap_fsetU1 {T U : choiceType} (F : T → set U) (x : T) (X : {fset T}) :
  \bigcap_(i in [set j | j \in x |` X ]%fset) F i =
  F x `&` \bigcap_(i in [set j | j \in X ]) F i.

Lemma bigcup_fsetD1 {T U : choiceType} (x : T) (F : T → set U) (X : {fset T}) :
    x \in X →
  \bigcup_(i in [set i | i \in X ]%fset) F i =
  F x `|` \bigcup_(i in [set i | i \in X `\ x ]%fset) F i.
Arguments bigcup_fsetD1 {T U} x.

Lemma bigcap_fsetD1 {T U : choiceType} (x : T) (F : T → set U) (X : {fset T}) :
    x \in X →
  \bigcap_(i in [set i | i \in X ]%fset) F i =
  F x `&` \bigcap_(i in [set i | i \in X `\ x ]%fset) F i.
Arguments bigcup_fsetD1 {T U} x.

Section bigcup_set.
Variables (T : choiceType) (U : Type).

Lemma bigcup_set_cond (s : seq T) (f : T → set U) (P : pred T) :
  \bigcup_(t in [set x | (x \in s ) && P x ]) (f t ) =
  \big[setU/set0]_(t <- s | P t) (f t).

Lemma bigcup_set (s : seq T) (f : T → set U) :
  \bigcup_(t in [set ` s ]) (f t ) = \big[setU/set0]_(t <- s) (f t).

Lemma bigcap_set_cond (s : seq T) (f : T → set U) (P : pred T) :
  \bigcap_(t in [set x | (x \in s ) && P x ]) (f t ) =
  \big[setI/setT]_(t <- s | P t) (f t).

Lemma bigcap_set (s : seq T) (f : T → set U) :
  \bigcap_(t in [set ` s ]) (f t ) = \big[setI/setT]_(t <- s) (f t).

End bigcup_set.

Lemma bigcup_pred [T : finType] [U : Type] (P : {pred T }) (f : T → set U) :
  \bigcup_(t in [set ` P ]) f t = \big[setU/set0]_(t in P) f t.

Section smallest.
Context {T} (C : set T → Prop) (G : set T).

Definition smallest := \bigcap_(A in [set M | C M ∧ G `<=` M ]) A.

Lemma sub_smallest X : X `<=` G → X `<=` smallest.

Lemma sub_gen_smallest : G `<=` smallest.

Lemma smallest_sub X : C X → G `<=` X → smallest `<=` X.

Lemma smallest_id : C G → smallest = G.

End smallest.
#[global] Hint Resolve sub_gen_smallest : core.

Lemma sub_smallest2r {T} (C : set T → Prop) G1 G2 :
   C (smallest C G2) → G1 `<=` G2 → smallest C G1 `<=` smallest C G2.

Lemma sub_smallest2l {T} (C1 C2 : set T → Prop) :
   (∀ G, C2 G → C1 G ) →
   ∀ G, smallest C1 G `<=` smallest C2 G.

Section bigop_nat_lemmas.
Context {T : Type}.
Implicit Types (A : set T) (F : nat → set T).

Lemma bigcup_mkord n F :
  \bigcup_(i in `I_n ) F i = \big[setU/set0]_(i < n) F i.

Lemma bigcap_mkord n F :
  \bigcap_(i in `I_n ) F i = \big[setI/setT]_(i < n) F i.

Lemma bigsetU_bigcup F n : \big[setU/set0]_(i < n) F i `<=` \bigcup_k F k.

Lemma bigsetU_bigcup2 (A B : set T) :
   \big[setU/set0]_(i < 2) bigcup2 A B i = A `|` B.

Lemma bigsetI_bigcap2 (A B : set T) :
   \big[setI/setT]_(i < 2) bigcap2 A B i = A `&` B.

Lemma bigcup_splitn n F :
  \bigcup_i F i = \big[setU/set0]_(i < n) F i `|` \bigcup_i F (n + i)%N.

Lemma bigcap_splitn n F :
  \bigcap_i F i = \big[setI/setT]_(i < n) F i `&` \bigcap_i F (n + i)%N.

Lemma subset_bigsetU F :
  {homo (fun n ⇒ \big[setU/set0]_(i < n) F i ) : n m / (n ≤ m)%N >-> n `<=` m }.

Lemma subset_bigsetI F :
  {homo (fun n ⇒ \big[setI/setT]_(i < n) F i ) : n m / (n ≤ m)%N >-> m `<=` n }.

Lemma subset_bigsetU_cond (P : pred nat) F :
  {homo (fun n ⇒ \big[setU/set0]_(i < n | P i) F i )
    : n m / (n ≤ m)%N >-> n `<=` m }.

Lemma subset_bigsetI_cond (P : pred nat) F :
  {homo (fun n ⇒ \big[setI/setT]_(i < n | P i) F i )
    : n m / (n ≤ m)%N >-> m `<=` n }.

End bigop_nat_lemmas.

Definition is_subset1 {T} (A : set T) := ∀ x y, A x → A y → x = y.
Definition is_fun {T1 T2} (f : T1 → T2 → Prop) := Logic.all (is_subset1 \o f).
Definition is_total {T1 T2} (f : T1 → T2 → Prop) := Logic.all (nonempty \o f).
Definition is_totalfun {T1 T2} (f : T1 → T2 → Prop) :=
  ∀ x, f x !=set0 ∧ is_subset1 (f x).

Definition xget {T : choiceType} x0 (P : set T) : T :=
  if pselect (∃ x : T , `[<P x >]) isn't left exP then x0
  else projT1 (sigW exP).

CoInductive xget_spec {T : choiceType} x0 (P : set T) : T → Prop → Type :=
| XGetSome x of x = xget x0 P & P x : xget_spec x0 P x True
| XGetNone of (∀ x, ¬ P x) : xget_spec x0 P x0 False.

Lemma xgetP {T : choiceType} x0 (P : set T) :
  xget_spec x0 P (xget x0 P) (P (xget x0 P)).

Lemma xgetPex {T : choiceType} x0 (P : set T) : (∃ x , P x ) → P (xget x0 P).

Lemma xgetI {T : choiceType} x0 (P : set T) (x : T): P x → P (xget x0 P).

Lemma xget_subset1 {T : choiceType} x0 (P : set T) (x : T) :
  P x → is_subset1 P → xget x0 P = x.

Lemma xget_unique {T : choiceType} x0 (P : set T) (x : T) :
  P x → (∀ y, P y → y = x ) → xget x0 P = x.

Lemma xgetPN {T : choiceType} x0 (P : set T) :
  (∀ x, ¬ P x ) → xget x0 P = x0.

Definition fun_of_rel {aT} {rT : choiceType} (f0 : aT → rT)
  (f : aT → rT → Prop) := fun x ⇒ xget (f0 x) (f x).

Lemma fun_of_relP {aT} {rT : choiceType} (f : aT → rT → Prop) (f0 : aT → rT) a :
  f a !=set0 → f a (fun_of_rel f0 f a).

Lemma fun_of_rel_uniq {aT} {rT : choiceType}
    (f : aT → rT → Prop) (f0 : aT → rT) a :
  is_subset1 (f a) → ∀ b, f a b → fun_of_rel f0 f a = b.

Lemma forall_sig T (A : set T) (P : {x | x \in A } → Prop) :
  (∀ u : {x | x \in A }, P u ) =
  (∀ u : T, ∀ (a : A u), P (exist _ u (mem_set a))).

Lemma in_setP {U} (A : set U) (P : U → Prop) :
  {in A , ∀ x, P x } ↔ ∀ x, A x → P x.

Lemma in_set2P {U V} (A : set U) (B : set V) (P : U → V → Prop) :
  {in A & B , ∀ x y, P x y } ↔ (∀ x y, A x → B y → P x y ).

Lemma in1TT [T1] [P1 : T1 → Prop] :
  {in [set : T1 ], ∀ x : T1, P1 x : Prop } → ∀ x : T1, P1 x : Prop.

Lemma in2TT [T1 T2] [P2 : T1 → T2 → Prop] :
  {in [set : T1 ] & [set : T2 ], ∀ (x : T1) (y : T2), P2 x y : Prop } →
  ∀ (x : T1) (y : T2), P2 x y : Prop.

Lemma in3TT [T1 T2 T3] [P3 : T1 → T2 → T3 → Prop] :
  {in [set : T1 ] & [set : T2 ] & [set : T3 ], ∀ (x : T1) (y : T2) (z : T3), P3 x y z : Prop } →
  ∀ (x : T1) (y : T2) (z : T3), P3 x y z : Prop.

Lemma inTT_bij [T1 T2 : Type] [f : T1 → T2] :
  {in [set : T1 ], bijective f } → bijective f.

Module Pointed.

Definition point_of (T : Type) := T.

Record class_of (T : Type) := Class {
  base : Choice.class_of T;
  mixin : point_of T
}.

Section ClassDef.

Structure type := Pack { sort; _ : class_of sort }.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c := cT return class_of cT in c.

Definition clone c of phant_id class c := @Pack T c.
Let xT := let: Pack T _ := cT in T.
Notation xclass := (class : class_of xT).

Definition pack m :=
  fun bT b of phant_id (Choice.class bT) b ⇒ @Pack T (Class b m).

Definition eqType := @Equality.Pack cT xclass.
Definition choiceType := @Choice.Pack cT xclass.

End ClassDef.

Module Exports.

Coercion sort : type >-> Sortclass.
Coercion base : class_of >-> Choice.class_of.
Coercion mixin : class_of >-> point_of.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Notation pointedType := type.
Notation PointedType T m := (@pack T m _ _ idfun).
Notation "[ 'pointedType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
  (at level 0, format "[ 'pointedType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'pointedType' 'of' T ]" := (@clone T _ _ id)
  (at level 0, format "[ 'pointedType' 'of' T ]") : form_scope.

End Exports.

End Pointed.

Export Pointed.Exports.

Definition point {M : pointedType} : M := Pointed.mixin (Pointed.class M).

Canonical arrow_pointedType (T : Type) (T' : pointedType) :=
  PointedType (T → T') (fun ⇒ point).

Definition dep_arrow_pointedType (T : Type) (T' : T → pointedType) :=
  Pointed.Pack
   (Pointed.Class (dep_arrow_choiceClass T') (fun i ⇒ @point (T' i))).

Canonical bool_pointedType := PointedType bool false.
Canonical Prop_pointedType := PointedType Prop False.
Canonical nat_pointedType := PointedType nat 0%N.
Canonical prod_pointedType (T T' : pointedType) :=
  PointedType (T × T') (point , point ).
Canonical matrix_pointedType m n (T : pointedType) :=
  PointedType 'M[T]_(m, n) (\matrix_(_, _) point)%R.
Canonical option_pointedType (T : choiceType) := PointedType (option T) None.

Notation get := (xget point).
Notation "[ 'get' x | E ]" := (get [set x | E])
  (at level 0, x name, format "[ 'get' x | E ]", only printing) : form_scope.
Notation "[ 'get' x : T | E ]" := (get (fun x : T ⇒ E))
  (at level 0, x name, format "[ 'get' x : T | E ]", only parsing) : form_scope.
Notation "[ 'get' x | E ]" := (get (fun x ⇒ E))
  (at level 0, x name, format "[ 'get' x | E ]") : form_scope.

Section PointedTheory.

Context {T : pointedType}.

Lemma getPex (P : set T) : (∃ x , P x ) → P (get P).

Lemma getI (P : set T) (x : T): P x → P (get P).

Lemma get_subset1 (P : set T) (x : T) : P x → is_subset1 P → get P = x.

Lemma get_unique (P : set T) (x : T) :
   P x → (∀ y, P y → y = x ) → get P = x.

Lemma getPN (P : set T) : (∀ x, ¬ P x ) → get P = point.

End PointedTheory.

Variant squashed T : Prop := squash (x : T).
Arguments squash {T} x.
Notation "$| T |" := (squashed T) : form_scope.
Tactic Notation "squash" uconstr(x) := (∃; refine x) ||
   match goal with |- $| ?T | ⇒ ∃; refine [the T of x] end.

Definition unsquash {T} (s : $|T |) : T :=
  projT1 (cid (let: squash x := s in @ex_intro T _ x isT)).
Lemma unsquashK {T} : cancel (@unsquash T) squash.

Empty types

Module Empty.

Definition mixin_of T := T → False.

Section EqMixin.
Variables (T : Type) (m : mixin_of T).
Definition eq_op (x y : T) := true.
Lemma eq_opP : Equality.axiom eq_op.
Definition eqMixin := EqMixin eq_opP.
End EqMixin.

Section ChoiceMixin.
Variables (T : Type) (m : mixin_of T).
Definition find of pred T & nat : option T := None.
Lemma findP (P : pred T) (n : nat) (x : T) : find P n = Some x → P x.
Lemma ex_find (P : pred T) : (∃ x : T , P x ) → ∃ n : nat , find P n.
Lemma eq_find (P Q : pred T) : P =1 Q → find P =1 find Q.
Definition choiceMixin := Choice.Mixin findP ex_find eq_find.
End ChoiceMixin.

Section CountMixin.
Variables (T : Type) (m : mixin_of T).
Definition pickle : T → nat := fun ⇒ 0%N.
Definition unpickle : nat → option T := fun ⇒ None.
Lemma pickleK : pcancel pickle unpickle.
Definition countMixin := CountMixin pickleK.
End CountMixin.

Section FinMixin.
Variables (T : countType) (m : mixin_of T).
Lemma fin_axiom : Finite.axiom ([::] : seq T).
Definition finMixin := FinMixin fin_axiom.
End FinMixin.

Section ClassDef.

Record class_of T := Class {
  base : Finite.class_of T;
  mixin : mixin_of T
}.

Structure type : Type := Pack {sort; _ : class_of sort}.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c.

Definition pack (m0 : mixin_of T) :=
  fun bT b & phant_id (Finite.class bT) b ⇒
  fun m & phant_id m0 m ⇒ Pack (@Class T b m).

Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition countType := @Countable.Pack cT class.
Definition finType := @Finite.Pack cT class.

End ClassDef.

Module Import Exports.
Coercion base : class_of >-> Finite.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion countType : type >-> Countable.type.
Canonical countType.
Coercion finType : type >-> Finite.type.
Canonical finType.
Notation emptyType := type.
Notation EmptyType T m := (@pack T m _ _ id _ id).
Notation "[ 'emptyType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
  (at level 0, format "[ 'emptyType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'emptyType' 'of' T ]" := (@clone T _ _ id)
  (at level 0, format "[ 'emptyType' 'of' T ]") : form_scope.
Coercion eqMixin : mixin_of >-> Equality.mixin_of.
Coercion choiceMixin : mixin_of >-> Choice.mixin_of.
Coercion countMixin : mixin_of >-> Countable.mixin_of.
End Exports.

End Empty.
Export Empty.Exports.

Definition False_emptyMixin : Empty.mixin_of False := id.
Canonical False_eqType := EqType False False_emptyMixin.
Canonical False_choiceType := ChoiceType False False_emptyMixin.
Canonical False_countType := CountType False False_emptyMixin.
Canonical False_finType := FinType False (Empty.finMixin False_emptyMixin).
Canonical False_emptyType := EmptyType False False_emptyMixin.

Definition void_emptyMixin : Empty.mixin_of void := @of_void _.
Canonical void_emptyType := EmptyType void void_emptyMixin.

Definition no {T : emptyType} : T → False :=
  let: Empty.Pack _ (Empty.Class _ f) := T in f.
Definition any {T : emptyType} {U} : T → U := @False_rect _ \o no.

Lemma empty_eq0 {T : emptyType} : all_equal_to (set0 : set T).

Definition quasi_canonical_of T C (sort : C → T) (alt : emptyType → T):=
    ∀ (G : T → Type), (∀ s : emptyType, G (alt s)) → (∀ x, G (sort x)) →
  ∀ x, G x.
Notation quasi_canonical_ sort alt := (@quasi_canonical_of _ _ sort alt).
Notation quasi_canonical T C := (@quasi_canonical_of T C id id).

Lemma qcanon T C (sort : C → T) (alt : emptyType → T) :
    (∀ x, (∃ y : emptyType , alt y = x ) + (∃ y , sort y = x )) →
  quasi_canonical_ sort alt.
Arguments qcanon {T C sort alt} x.

Lemma choicePpointed : quasi_canonical choiceType pointedType.

Lemma eqPpointed : quasi_canonical eqType pointedType.
Lemma Ppointed : quasi_canonical Type pointedType.

Section partitions.

Definition trivIset T I (D : set I) (F : I → set T) :=
  ∀ i j : I, D i → D j → F i `&` F j !=set0 → i = j.

Lemma trivIset_set0 {I T} (D : set I) : trivIset D (fun ⇒ set0 : set T).

Lemma trivIsetP {T} {I : eqType} {D : set I} {F : I → set T} :
  trivIset D F ↔
  ∀ i j : I, D i → D j → i != j → F i `&` F j = set0.

Lemma trivIset_bigsetUI T (D : {pred nat }) (F : nat → set T) : trivIset D F →
  ∀ n m, D m → n ≤ m → \big[setU/set0]_(i < n | D i) F i `&` F m = set0.

Lemma trivIset_setIl (T I : Type) (D : set I) (F : I → set T) (G : I → set T) :
  trivIset D F → trivIset D (fun i ⇒ G i `&` F i).

Lemma trivIset_setIr (T I : Type) (D : set I) (F : I → set T) (G : I → set T) :
  trivIset D F → trivIset D (fun i ⇒ F i `&` G i).

#[deprecated(note="Use trivIset_setIl instead")]
Lemma trivIset_setI T I D (F : I → set T) X :
  trivIset D F → trivIset D (fun i ⇒ X `&` F i).

Lemma sub_trivIset I T (D D' : set I) (F : I → set T) :
  D `<=` D' → trivIset D' F → trivIset D F.

Lemma trivIset_bigcup2 T (A B : set T) :
  (A `&` B = set0 ) = trivIset setT (bigcup2 A B).

Lemma trivIset_image (T I I' : Type) (D : set I) (f : I → I') (F : I' → set T) :
  trivIset D (F \o f) → trivIset (f @` D) F.
Arguments trivIset_image {T I I'} D f F.

Lemma trivIset_comp (T I I' : Type) (D : set I) (f : I → I') (F : I' → set T) :
    {in D &, injective f } →
  trivIset D (F \o f) = trivIset (f @` D) F.

Definition cover T I D (F : I → set T) := \bigcup_(i in D ) F i.

Lemma cover_restr T I D' D (F : I → set T) :
  D `<=` D' → (∀ i, D' i → ¬ D i → F i = set0 ) →
  cover D F = cover D' F.

Lemma eqcover_r T I D (F G : I → set T) :
  [set F i | i in D ] = [set G i | i in D ] →
  cover D F = cover D G.

Definition partition T I D (F : I → set T) (A : set T) :=
  [/\ cover D F = A , trivIset D F & ∀ i, D i → F i !=set0 ].

Definition pblock_index T (I : pointedType) D (F : I → set T) (x : T) :=
  [get i | D i ∧ F i x ].

Definition pblock T (I : pointedType) D (F : I → set T) (x : T) :=
  F (pblock_index D F x).

TODO: theory of trivIset, cover, partition, pblock_index and pblock

Notation trivIsets X := (trivIset X id).

Lemma trivIset_sets T I D (F : I → set T) :
trivIset D F → trivIsets [set F i | i in D ].

Lemma trivIset_widen T I D' D (F : I → set T) :

D `<=` D' -> (forall i, D i -> ~ D' i -> F i !=set0) ->

  D `<=` D' → (∀ i, D' i → ¬ D i → F i = set0 ) →
  trivIset D F = trivIset D' F.

Lemma perm_eq_trivIset {T : eqType} (s1 s2 : seq (set T)) (D : set nat) :
  [set k | (k < size s1)%N] `<=` D → perm_eq s1 s2 →
  trivIset D (fun i ⇒ nth set0 s1 i) → trivIset D (fun i ⇒ nth set0 s2 i).

End partitions.

Definition total_on T (A : set T) (R : T → T → Prop) :=
  ∀ s t, A s → A t → R s t ∨ R t s.

Section ZL.

Variable (T : Type) (t0 : T) (R : T → T → Prop).
Hypothesis (Rrefl : ∀ t, R t t).
Hypothesis (Rtrans : ∀ r s t, R r s → R s t → R r t).
Hypothesis (Rantisym : ∀ s t, R s t → R t s → s = t).
Hypothesis (tot_lub : ∀ A : set T, total_on A R → ∃ t ,
  (∀ s, A s → R s t ) ∧ ∀ r, (∀ s, A s → R s r ) → R t r).
Hypothesis (Rsucc : ∀ s, ∃ t , R s t ∧ s ≠ t ∧
  ∀ r, R s r → R r t → r = s ∨ r = t).

Let Teq := @gen_eqMixin T.
Let Tch := @gen_choiceMixin T.
Let Tp := Pointed.Pack (Pointed.Class (Choice.Class Teq Tch) t0).
Let lub := fun A : {A : set T | total_on A R } ⇒
  [get t : Tp | (∀ s, sval A s → R s t ) ∧
    ∀ r, (∀ s, sval A s → R s r ) → R t r ].
Let succ := fun s ⇒ [get t : Tp | R s t ∧ s ≠ t ∧
  ∀ r, R s r → R r t → r = s ∨ r = t ].

Inductive tower : set T :=
  | Lub : ∀ A, sval A `<=` tower → tower (lub A)
  | Succ : ∀ t, tower t → tower (succ t).

Lemma ZL' : False.

End ZL.

Lemma Zorn T (R : T → T → Prop) :
  (∀ t, R t t ) → (∀ r s t, R r s → R s t → R r t ) →
  (∀ s t, R s t → R t s → s = t ) →
  (∀ A : set T, total_on A R → ∃ t , ∀ s, A s → R s t ) →
  ∃ t , ∀ s, R t s → s = t.

Definition premaximal T (R : T → T → Prop) (t : T) :=
  ∀ s, R t s → R s t.

Lemma ZL_preorder T (t0 : T) (R : T → T → Prop) :
  (∀ t, R t t ) → (∀ r s t, R r s → R s t → R r t ) →
  (∀ A : set T, total_on A R → ∃ t , ∀ s, A s → R s t ) →
  ∃ t , premaximal R t.

Section UpperLowerTheory.
Import Order.TTheory.
Variables (d : unit) (T : porderType d).
Implicit Types (A : set T) (x y z : T).

Definition ubound A : set T := [set y | ∀ x, A x → (x ≤ y)%O].
Definition lbound A : set T := [set y | ∀ x, A x → (y ≤ x)%O].

Lemma ubP A x : (∀ y, A y → (y ≤ x)%O) ↔ ubound A x.

Lemma lbP A x : (∀ y, A y → (x ≤ y)%O) ↔ lbound A x.

Lemma ub_set1 x y : ubound [set x ] y = (x ≤ y)%O.

Lemma lb_set1 x y : lbound [set x ] y = (x ≥ y)%O.

Lemma lb_ub_set1 x y : lbound (ubound [set x ]) y → (y ≤ x)%O.

Lemma ub_lb_set1 x y : ubound (lbound [set x ]) y → (x ≤ y)%O.

Lemma lb_ub_refl x : lbound (ubound [set x ]) x.

Lemma ub_lb_refl x : ubound (lbound [set x ]) x.

Lemma ub_lb_ub A x y : ubound A y → lbound (ubound A) x → (x ≤ y)%O.

Lemma lb_ub_lb A x y : lbound A y → ubound (lbound A) x → (y ≤ x)%O.

down set (i.e., generated order ideal) i.e. down A := { x | exists y, y \in A /\ x <= y}

Definition down A : set T := [set x | ∃ y , A y ∧ (x ≤ y)%O].

Definition has_ubound A := ubound A !=set0.
Definition has_sup A := A !=set0 ∧ has_ubound A.
Definition has_lbound A := lbound A !=set0.
Definition has_inf A := A !=set0 ∧ has_lbound A.

Lemma has_ub_set1 x : has_ubound [set x ].

Lemma has_inf0 : ¬ has_inf (@set0 T).

Lemma has_sup0 : ¬ has_sup (@set0 T).

Lemma has_sup1 x : has_sup [set x ].

Lemma has_inf1 x : has_inf [set x ].

Lemma subset_has_lbound A B : A `<=` B → has_lbound B → has_lbound A.

Lemma subset_has_ubound A B : A `<=` B → has_ubound B → has_ubound A.

Lemma downP A x : (exists2 y , A y & (x ≤ y)%O) ↔ down A x.

Definition isLub A m := ubound A m ∧ ∀ b, ubound A b → (m ≤ b)%O.

Definition supremums A := ubound A `&` lbound (ubound A).

Lemma supremums1 x : supremums [set x ] = [set x ].

Lemma is_subset1_supremums A : is_subset1 (supremums A).

Definition supremum x0 A := if A == set0 then x0 else xget x0 (supremums A).

Lemma supremum_out x0 A : ¬ has_sup A → supremum x0 A = x0.

Lemma supremum0 x0 : supremum x0 set0 = x0.

Lemma supremum1 x0 x : supremum x0 [set x ] = x.

Definition infimums A := lbound A `&` ubound (lbound A).

Lemma infimums1 x : infimums [set x ] = [set x ].

Lemma is_subset1_infimums A : is_subset1 (infimums A).

Definition infimum x0 A := if A == set0 then x0 else xget x0 (infimums A).

End UpperLowerTheory.

Section UpperLowerOrderTheory.
Import Order.TTheory.
Variables (d : unit) (T : orderType d).
Implicit Types (A : set T) (x y z : T).

Lemma ge_supremum_Nmem x0 A t :
  supremums A !=set0 → A t → (supremum x0 A ≥ t)%O.

Lemma le_infimum_Nmem x0 A t :
  infimums A !=set0 → A t → (infimum x0 A ≤ t)%O.

End UpperLowerOrderTheory.

Lemma nat_supremums_neq0 (A : set nat) : ubound A !=set0 → supremums A !=set0.

Definition meets T (F G : set (set T)) :=
  ∀ A B, F A → G B → A `&` B !=set0.

Notation "F `#` G" := (meets F G) : classical_set_scope.

Section meets.

Lemma meetsC T (F G : set (set T)) : F `#` G = G `#` F.

Lemma sub_meets T (F F' G G' : set (set T)) :
  F `<=` F' → G `<=` G' → F' `#` G' → F `#` G.

Lemma meetsSr T (F G G' : set (set T)) :
  G `<=` G' → F `#` G' → F `#` G.

Lemma meetsSl T (G F F' : set (set T)) :
  F `<=` F' → F' `#` G → F `#` G.

End meets.

Fact set_display : unit.

Module SetOrder.
Module Internal.
Section SetOrder.

Context {T : Type}.
Implicit Types A B : set T.

Lemma le_def A B : `[< A `<=` B >] = (A `&` B == A ).

Lemma lt_def A B : `[< A `<` B >] = (B != A ) && `[< A `<=` B >].

Lemma joinKI B A : A `&` (A `|` B ) = A.

Lemma meetKU B A : A `|` (A `&` B ) = A.

Definition orderMixin := @MeetJoinMixin _ _ (fun A B ⇒ `[<proper A B >]) setI
  setU le_def lt_def (@setIC _) (@setUC _) (@setIA _) (@setUA _) joinKI meetKU
  (@setIUl _) setIid.

Lemma SetOrder_sub0set A : (set0 ≤ A)%O.

Lemma SetOrder_setTsub A : (A ≤ setT)%O.

Lemma subKI A B : B `&` (A `\` B ) = set0.

Lemma joinIB A B : (A `&` B ) `|` A `\` B = A.

End SetOrder.
End Internal.

Module Exports.

Canonical Internal.porderType.
Canonical Internal.latticeType.
Canonical Internal.distrLatticeType.
Canonical Internal.bLatticeType.
Canonical Internal.tbLatticeType.
Canonical Internal.bDistrLatticeType.
Canonical Internal.tbDistrLatticeType.
Canonical Internal.cbDistrLatticeType.
Canonical Internal.ctbDistrLatticeType.

Section exports.
Context {T : Type}.
Implicit Types A B : set T.

Lemma subsetEset A B : (A ≤ B)%O = (A `<=` B ) :> Prop.

Lemma properEset A B : (A < B)%O = (A `<` B ) :> Prop.

Lemma subEset A B : (A `\` B)%O = (A `\` B ).

Lemma complEset A : (~` A)%O = ~` A.

Lemma botEset : 0%O = @set0 T.

Lemma topEset : 1%O = @setT T.

Lemma meetEset A B : (A `&` B)%O = (A `&` B ).

Lemma joinEset A B : (A `|` B)%O = (A `|` B ).

Lemma subsetPset A B : reflect (A `<=` B) (A ≤ B)%O.

Lemma properPset A B : reflect (A `<` B) (A < B)%O.

End exports.
End Exports.
End SetOrder.
Export SetOrder.Exports.

Section section.
Variables (T1 T2 : Type).
Implicit Types (A : set (T1 × T2)) (x : T1) (y : T2).

Definition xsection A x := [set y | (x , y ) \in A ].

Definition ysection A y := [set x | (x , y ) \in A ].

Lemma xsection0 x : xsection set0 x = set0.

Lemma ysection0 y : ysection set0 y = set0.

Lemma in_xsectionM X1 X2 x : x \in X1 → xsection (X1 `*` X2) x = X2.

Lemma in_ysectionM X1 X2 y : y \in X2 → ysection (X1 `*` X2) y = X1.

Lemma notin_xsectionM X1 X2 x : x \notin X1 → xsection (X1 `*` X2) x = set0.

Lemma notin_ysectionM X1 X2 y : y \notin X2 → ysection (X1 `*` X2) y = set0.

Lemma xsection_bigcup (F : nat → set (T1 × T2)) x :
  xsection (\bigcup_n F n) x = \bigcup_n xsection (F n) x.

Lemma ysection_bigcup (F : nat → set (T1 × T2)) y :
  ysection (\bigcup_n F n) y = \bigcup_n ysection (F n) y.

Lemma trivIset_xsection (F : nat → set (T1 × T2)) x : trivIset setT F →
  trivIset setT (fun n ⇒ xsection (F n) x).

Lemma trivIset_ysection (F : nat → set (T1 × T2)) y : trivIset setT F →
  trivIset setT (fun n ⇒ ysection (F n) y).

Lemma le_xsection x : {homo xsection ^~ x : X Y / X `<=` Y >-> X `<=` Y }.

Lemma le_ysection y : {homo ysection ^~ y : X Y / X `<=` Y >-> X `<=` Y }.

Lemma xsectionD X Y x : xsection (X `\` Y) x = xsection X x `\` xsection Y x.

Lemma ysectionD X Y y : ysection (X `\` Y) y = ysection X y `\` ysection Y y.

End section.