Module mathcomp.classical.classical_sets

From HB Require Import structures.
From mathcomp Require Import boot order ssralg matrix finmap ssrnum.
From mathcomp Require Import ssrint rat interval.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import boolp wochoice.

# Set Theory This file develops a basic theory of sets and types equipped with a canonical inhabitant (pointed types). 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$. 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 Examples of notations: | Rocq notatons | | Meaning | |-----------------------------:|---|:------------------------------------ | set0 |==| $\emptyset$ | [set: A] |==| the full set of elements of type A | `` `\|` `` |==| $\cup$ | `` `&` `` |==| $\cap$ | `` `\` `` |==| set difference | `` `+` `` |==| symmetric difference | `` ~` `` |==| set complement | `` `<=` `` |==| $\subseteq$ | `` f @` A `` |==| image by f of A | `` f @^-1` A `` |==| preimage by f of A | [set x] |==| the singleton set $\{x\}$ | [set~ x] |==| the complement of $\{x\}$ | [set E \| x in P] |==| the set of E with x ranging in P | range f |==| image by f of the full set | \big[setU/set0]_(i <- s \| P i) f i |==| finite union | \bigcup_(k in P) F k |==| arbitrary union | \bigcap_(k in P) F k |==| arbitrary intersection | trivIset D F |==| F is a sequence of pairwise disjoint | | | sets indexed over the domain D Detailed documentation: ## 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 `I_n := [set k | k < n] \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 < n) F := \bigcup_(i in `I_n) F \bigcup_(i >= n) F := \bigcup_(i in [set i | i >= n]) F \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 < n) F := \bigcap_(i in `I_n) F \bigcap_(i >= n) F := \bigcap_(i in [set i | i >= n]) F \bigcap_i F == same as before with T left implicit ``` ### About sets of sets ``` set_system T := set (set T) setI_closed G == the set of sets G is closed under finite intersection setU_closed G == the set of sets G is closed under finite union rectangle X Y := [set U `*` V | U in X & V in Y] preimage_set_system D f G == set system of the preimages by f of sets in G image_set_system D f G == set system of the sets with a preimage by f in G cross f g X Y := preimage_set_system setT f X `|` preimage_set_system setT g Y X `x` Y := cross fst snd X Y ``` ``A `+ B`` : $\{ x + y | x\in A, x\in B\}$ ``` R ^nat == notation for the type of sequences, i.e., functions of type nat -> R bigcup2 A B == the sequence A, B, 0, 0, ... bigcup2 A B == the sequence A, B, T, T, ... smallest C G := \bigcap_(A in [set M | C M /\ G `<=` M]) A A `<=` B <-> A is included in B A `<` B := A `<=` B /\ ~ (B `<=` A) A `<=>` B <-> double inclusion A `<=` B and B `<=` A f @^-1` A == preimage of A by f f @` A == image of A by f This is a 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[] 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 seqDU F := sequence F_0, F_1\F_0, F_2\(F_0 U F_1),... seqD F == the sequence F_0, F_1 \ F_0, F_2 \ F_1,... ``` ## Pointed types ``` pointedType == interface type for types equipped with a canonical inhabitant The HB class is Pointed. 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. ``` ## squash/unsquash ``` $| T | == the type `T : Type` is inhabited $| T | has type `Prop`. $| T | is a notation for `squashed T`. squash x == object of type $| T | (with x : T) unsquash s == extract an inhabitant of type `T` (with s : $| T |) ``` Tactic: - squash x: solves a goal $| T | by instantiating with x or [the T of x] ## Pairwise-disjoint sets ``` 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) maximal_disjoint_subcollection F A B == A is a maximal (for inclusion) disjoint subcollection of the collection B of elements in F : I -> set T ``` ## 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 ``` ## Relations Notations for composition and inverse (scope: relation_scope): ``` B \; A == [set x | exists z, A (x.1, z) & B (z, x.2)] A^-1 == [set xy | A (xy.2, xy.1)] ```

Unset SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Declare Scope classical_set_scope.
Declare Scope relation_scope.
Delimit Scope relation_scope with relation.

Reserved Notation "R ^nat".
Reserved Notation "[ 'set' x : T | P ]" (only parsing).
Reserved Notation "[ 'set' x | P ]" (format "[ 'set' x | P ]").
Reserved Notation "[ 'set' E | x 'in' A ]"
  (format "[ '[hv' 'set' E '/ ' | x 'in' A ] ']'").
Reserved Notation "[ 'set' E | x 'in' A & y 'in' B ]"
  (format "[ '[hv' 'set' E '/ ' | x 'in' A & y 'in' B ] ']'").
Reserved Notation "[ 'set' a ]" (format "[ 'set' a ]").
Reserved Notation "[ 'set' : T ]" (format "[ 'set' : T ]").
Reserved Notation "[ 'set' a : T ]" (format "[ 'set' a : T ]").
Reserved Notation "A `|` B" (at level 52, left associativity).
Reserved Notation "a |` A" (at level 52, left associativity).
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" (format "A .`1").
Reserved Notation "A .`2" (format "A .`2").
Reserved Notation "~` A" (at level 35, right associativity).
Reserved Notation "[ 'set' ~ a ]" (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 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 ]" (format "[ 'set`' p ]").
Reserved Notation "[ 'disjoint' A & B ]"
  (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").
Reserved Notation "A `x` B"  (at level 46, left associativity).
Reserved Notation "A `+ B" (at level 50).

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

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

Proof.

by rewrite propeqE; split => [] /asboolP. Qed.

Definition := (inE, in_setE).

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

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

Notation := (mkset (fun : T => P)) : classical_set_scope.
Notation := [set : _ | P] : classical_set_scope.

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

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

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

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

Definition := [set _ : T | True].
Definition := [set _ : T | False].
Definition ( : T) := [set : T | x = t].
Definition := [set | A x /\ B x].
Definition := [set | A x \/ B x].
Definition := exists , A a.
Definition := [set | ~ A a].
Definition := [set | A x /\ ~ B x].
Definition ( : set T1) ( : set T2) := [set | A1 z.1 /\ A2 z.2].
Definition ( : set (T1 * T2)) := [set | exists , A (x, y)].
Definition ( : set (T1 * T2)) := [set | exists , A (x, y)].
Definition ( : set T1) ( : T1 -> set T2) :=
  [set | A1 z.1 /\ A2 z.1 z.2].
Definition ( : T2 -> set T1) ( : set T2) :=
  [set | A1 z.2 z.1 /\ A2 z.2].

Lemma ( : T -> Prop) : [set | P x] x = P x.

Proof.

by []. Qed.

Definition ( : set I) ( : I -> set T) :=
[set | forall , P i -> F i a].
Definition ( : set I) ( : I -> set T) :=
[set | exists2 , P i & F i a].

Definition := forall , A t -> B t.
Local Notation := (subset A B).

Lemma : {subset A <= B} <-> (A `<=` B).

Proof.

by split => + x => /(_ x); rewrite ?inE. Qed.

Definition := setI A B == set0.

Definition := 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 setX _ _ _ _ _ /.
Arguments setXR _ _ _ _ _ /.
Arguments setXL _ _ _ _ _ /.
Arguments fst_set _ _ _ _ /.
Arguments snd_set _ _ _ _ /.
Arguments subsetP {T A B}.

Notation F := [set F i | in setT].
Notation := (set1 a) : classical_set_scope.
Notation := [set (a : T)] : classical_set_scope.
Notation := (@setT T) : classical_set_scope.
Notation := (setU A B) : classical_set_scope.
Notation := ([set a] `|` A) : classical_set_scope.
Notation :=
  (setU .. (a1 |` [set a2]) .. [set an]) : classical_set_scope.
Notation := (setI A B) : classical_set_scope.
Notation := (setX A B) : classical_set_scope.
Notation := (fst_set A) : classical_set_scope.
Notation := (snd_set A) : classical_set_scope.
Notation := (setXR A B) : classical_set_scope.
Notation := (setXL A B) : classical_set_scope.
Notation := (setC A) : classical_set_scope.
Notation := (~` [set a]) : classical_set_scope.
Notation := (setD A B) : classical_set_scope.
Notation := (A `\` [set a]) : classical_set_scope.
Notation := (disj_set A B) : classical_set_scope.

Definition { : Type} ( : set T) := (A `\` B) `|` (B `\` A).
Arguments setY _ _ _ _ /.
Notation := (setY A B) : classical_set_scope.

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

Notation :=
  (bigcup P (fun => F)) : classical_set_scope.
Notation :=
  (\bigcup_( in @setT T) F) : classical_set_scope.
Notation :=
  (\bigcup_( in `I_n) F) : classical_set_scope.
Notation :=
  (\bigcup_( in [set | (n <= i)%N]) F) : classical_set_scope.
Notation := (\bigcup_( : _) F) : classical_set_scope.
Notation :=
  (bigcap P (fun => F)) : classical_set_scope.
Notation :=
  (\bigcap_( in @setT T) F) : classical_set_scope.
Notation :=
  (\bigcap_( in `I_n) F) : classical_set_scope.
Notation :=
  (\bigcap_( in [set | (n <= i)%N]) F) : classical_set_scope.
Notation := (\bigcap_( : _) F) : classical_set_scope.

Notation := (subset A B) : classical_set_scope.
Notation := (proper A B) : classical_set_scope.

Notation := ((A `<=` B) /\ (B `<=` A)) : classical_set_scope.
Notation := (preimage f A) : classical_set_scope.
Notation := (image A f) (only parsing) : classical_set_scope.
Notation := (nonempty A) : classical_set_scope.

Notation := [set | is_true (x \in p)] : classical_set_scope.
Notation := (fun => [set` i]).

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

Lemma : [set: nat] !=set0

Proof.

by exists 1%N. Qed.

#[global] Hint Resolve nat_nonempty : core.

Lemma { : eqType} ( : T) ( : T) : (x \in [set a]) = (x == a).

Proof.

by apply/(sameP _ idP)/(equivP idP); rewrite inE eq_opE. Qed.

Lemma ( : porderType d) ( : T -> T -> Prop) ( : interval T) :
[set` j] `<=` [set` i] ->
{in i &, forall , P x y} -> {in j &, forall , P x y}.

Proof.

by move=> ji + x y xj yj; apply; exact: ji. Qed.

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

Proof.

by rewrite inE. Qed.

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

Proof.

by rewrite predeqE => t; split => [|?]; rewrite /= in_itv/= andbT.
Qed.

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

Proof.

by rewrite predeqE => t; split => [|?]; rewrite /= in_itv/= andbT.
Qed.

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

Proof.

by rewrite predeqE => t; split => [|?]; rewrite /= in_itv. Qed.

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

Proof.

by rewrite predeqE => t; split => [|?]; rewrite /= in_itv. Qed.

Lemma ( : T -> Prop) : (forall : T, P x = Q x) ->
[set | P x] = [set | Q x].

Proof.

by move=> /funext->. Qed.

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

Definition {} { : predType T} { : pT} : x \in P -> { | x \in P} :=
exist (fun => x \in P) x.

Lemma { : Type} : @set0 T -> P

Proof.

by case=> x; rewrite inE. Qed.

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

Proof.

apply/funext=> -[x|]/=; apply/idP/idP; rewrite /pred_oapp/= inE //=.
- by move=> xD; exists x.
- by move=> [// + + [<-]].
- by case.
Qed.

Lemma { : Type} ( : set T) :
pred_oapp (mem D) = mem (some @` D)%classic.

Proof.

by rewrite pred_oappE; apply/funext => x/=; apply/idP/idP; rewrite ?inE;
move=> [y/= ]; rewrite ?in_setE; exists y; rewrite ?in_setE.
Qed.

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

Lemma {} { : T} : A u -> u \in A

Proof.

by rewrite inE. Qed.

Lemma {} { : T} : u \in A -> A u

Proof.

by rewrite inE. Qed.

#[deprecated(since="mathcomp-analysis 1.16.0", use=in_setT)]
Lemma ( : T) : u \in [set: T]

Proof.

by rewrite inE. Qed.

Lemma {} { : T} : cancel (@mem_set A u) set_mem

Proof.

by []. Qed.

Lemma {} { : T} : cancel (@set_mem A u) mem_set

Proof.

by []. Qed.

Lemma ( : set T) ( : T) : ~ A u -> (u \in A) = false.

Proof.

by apply: contra_notF; rewrite inE. Qed.

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

Proof.

by apply/propext; split=> /asboolPn. Qed.

Lemma ( : set T) : A != setT <-> exists , ~ A t.

Proof.

split => [/negP|[t]]; last by apply: contra_notP => /negP/negPn/eqP ->.
apply: contra_notP => /forallNP h.
by apply/eqP; rewrite predeqE => t; split => // _; apply: contrapT.
Qed.

#[deprecated(note="Use setTPn instead")]
Notation := setTPn (only parsing).

Lemma ( : T) : (x \in set0) = false

Proof.

by rewrite memNset. Qed.

Lemma ( : T) : x \in setT

Proof.

by rewrite mem_set. Qed.

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

Proof.

by apply/idP/idP; rewrite inE notin_setE. Qed.

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

Proof.

by apply/idP/andP; rewrite !inE. Qed.

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

Proof.

by apply/idP/andP; rewrite !inE notin_setE. Qed.

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

Proof.

by apply/idP/orP; rewrite !inE. Qed.

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

Proof.

by apply/idP/andP; rewrite !inE. Qed.

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

Proof.

by apply: set_mem; apply: valP. Qed.

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

Proof.

rewrite propeqE; split => [->|[AB BA]]; [by split|].
by rewrite predeqE => t; split=> [/AB|/BA].
Qed.

Lemma : (A = B) <-> (A `<=>` B)

Proof.

by rewrite eqEsubset. Qed.

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

Proof.

by apply/seteqP; split. Qed.

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

Proof.

by apply/seteqP; split. Qed.

Lemma ( : {pred T}) : [set` predC P] = ~` [set` P].

Proof.

by apply/seteqP; split => t /negP. Qed.

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

Proof.

by apply/predeqP => x; split; rewrite /= inE => /andP. Qed.

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

Proof.

by apply/predeqP => x; split; rewrite /= inE => /orP. Qed.

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

Proof.

by rewrite [LHS]set_true. Qed.

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

Proof.

by rewrite [LHS]set_false. Qed.

Lemma : [set` A] = A.

Proof.

by apply/seteqP; split=> x/=; rewrite inE. Qed.

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

Proof.

by congr Mem; apply/funext=> x; apply/asboolP/idP. Qed.

Lemma : A `<=` A

Proof.

by []. Qed.

Lemma : A `<=` B -> B `<=` C -> A `<=` C.

Proof.

by move=> sAB sBC ? ?; apply/sBC/sAB. Qed.

Lemma : set0 `<=` A

Proof.

by []. Qed.

Lemma : A `<` B -> A `<=` B

Proof.

by case. Qed.

Lemma : ~ A `<` A

Proof.

by move=> [?]; apply. Qed.

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

Proof.

by rewrite predeqE; split => ?. Qed.

Lemma : involutive (@setC T).

Proof.

by move=> A; rewrite funeqE => t; rewrite /setC; exact: notLR. Qed.

Lemma : ~` setT = set0 :> set T

Proof.

by rewrite -setC0 setCK. Qed.

Definition := can_inj setCK.

Lemma : commutative (@setI T).

Proof.

by move=> A B; rewrite predeqE => ?; split=> [[]|[]]. Qed.

Lemma : A `<=` B -> C `&` A `<=` C `&` B.

Proof.

by move=> sAB t [Ct At]; split => //; exact: sAB. Qed.

Lemma : A `<=` B -> A `&` C `<=` B `&` C.

Proof.

by move=> sAB; rewrite -!(setIC C); apply setIS. Qed.

Lemma : A `<=` C -> B `<=` D -> A `&` B `<=` C `&` D.

Proof.

by move=> /(@setSI B) /subset_trans sAC /(@setIS C) /sAC. Qed.

Lemma : right_id setT (@setI T).

Proof.

by move=> A; rewrite predeqE => ?; split=> [[]|]. Qed.

Lemma : left_id setT (@setI T).

Proof.

by move=> A; rewrite predeqE => ?; split=> [[]|]. Qed.

Lemma : right_zero set0 (@setI T).

Proof.

by move=> A; rewrite predeqE => ?; split=> [[]|]. Qed.

Lemma : left_zero set0 (@setI T).

Proof.

by move=> A; rewrite setIC setI0. Qed.

Lemma : left_inverse set0 setC (@setI T).

Proof.

by move=> A; rewrite predeqE => ?; split => // -[]. Qed.

Lemma : right_inverse set0 setC (@setI T).

Proof.

by move=> A; rewrite setIC setICl. Qed.

Lemma : associative (@setI T).

Proof.

by move=> A B C; rewrite predeqE => ?; split=> [[? []]|[[]]]. Qed.

Lemma : left_commutative (@setI T).

Proof.

by move=> A B C; rewrite setIA [A `&` _]setIC -setIA. Qed.

Lemma : right_commutative (@setI T).

Proof.

by move=> A B C; rewrite setIC setICA setIA. Qed.

Lemma : @interchange (set T) setI setI.

Proof.

by move=> A B C D; rewrite -setIA [B `&` _]setICA setIA. Qed.

Lemma : idempotent_op (@setI T).

Proof.

by move=> A; rewrite predeqE => ?; split=> [[]|]. Qed.

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

Proof.

by rewrite setIA !(setIAC _ C) -(setIA _ C) setIid. Qed.

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

Proof.

by rewrite !(setIC A) setIIl. Qed.

Lemma : commutative (@setU T).

Proof.

move=> p q; rewrite /setU/mkset predeqE => a; tauto. Qed.

Lemma : A `<=` B -> C `|` A `<=` C `|` B.

Proof.

by move=> sAB t [Ct|At]; [left|right; exact: sAB]. Qed.

Lemma : A `<=` B -> A `|` C `<=` B `|` C.

Proof.

by move=> sAB; rewrite -!(setUC C); apply setUS. Qed.

Lemma : A `<=` C -> B `<=` D -> A `|` B `<=` C `|` D.

Proof.

by move=> /(@setSU B) /subset_trans sAC /(@setUS C) /sAC. Qed.

Lemma : left_zero setT (@setU T).

Proof.

by move=> A; rewrite predeqE => t; split; [case|left]. Qed.

Lemma : right_zero setT (@setU T).

Proof.

by move=> A; rewrite predeqE => t; split; [case|right]. Qed.

Lemma : left_id set0 (@setU T).

Proof.

by move=> A; rewrite predeqE => t; split; [case|right]. Qed.

Lemma : right_id set0 (@setU T).

Proof.

by move=> A; rewrite predeqE => t; split; [case|left]. Qed.

Lemma : left_inverse setT setC (@setU T).

Proof.

move=> A.
by rewrite predeqE => t; split => // _; case: (pselect (A t)); [right|left].
Qed.

Lemma : right_inverse setT setC (@setU T).

Proof.

by move=> A; rewrite setUC setUCl. Qed.

Lemma : associative (@setU T).

Proof.

move=> p q r; rewrite /setU/mkset predeqE => a; tauto. Qed.

Lemma : left_commutative (@setU T).

Proof.

by move=> A B C; rewrite setUA [A `|` _]setUC -setUA. Qed.

Lemma : right_commutative (@setU T).

Proof.

by move=> A B C; rewrite setUC setUCA setUA. Qed.

Lemma : @interchange (set T) setU setU.

Proof.

by move=> A B C D; rewrite -setUA [B `|` _]setUCA setUA. Qed.

Lemma : idempotent_op (@setU T).

Proof.

move=> p; rewrite /setU/mkset predeqE => a; tauto. Qed.

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

Proof.

by rewrite setUA !(setUAC _ C) -(setUA _ C) setUid. Qed.

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

Proof.

by rewrite !(setUC A) setUUl. Qed.

Lemma :
(forall , (~` B) x -> A x = C x) -> (A `|` B) = (C `|` B).

Proof.

move=> h; apply/seteqP; split => [x [Ax|Bx]|x [Cx|Bx]]; [|by right| |by right].
- by have [|/h {}h] := pselect (B x); [by right|left; rewrite -h].
- by have [|/h {}h] := pselect (B x); [by right|left; rewrite h].
Qed.

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

Proof.

by []. Qed.

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

Proof.

apply/seteqP; split => x /=; first tauto.
#[warnings="-deprecated-syntactic-definition"] by move=> [[a|c]]; rewrite not_andE notE; tauto.
Qed.

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

Proof.

by rewrite setUC setUDl setUC. Qed.

Lemma : A `<=` B -> A `|` (B `\` A) = B.

Proof.

move=> AB; apply/seteqP; split=> [x [/AB//|[//]]|x Bx].
by have [Ax|nAx] := pselect (A x); [left|right].
Qed.

Lemma : A `<=` B -> (B `\` A) `|` A = B.

Proof.

by move=> /setDUK; rewrite setUC. Qed.

Lemma : A `<=` B -> B `<=` C -> C `\` A = (C `\` B) `|` (B `\` A).

Proof.

move=> AB BC; apply/seteqP; split.
move=> x [Cx Ax].
by have [Bx|Bx] := pselect (B x); [right|left].
move=> x [[Cx Bx]|[Bx Ax]].
- by split => // /AB.
- by split => //; exact/BC.
Qed.

Lemma : A `\` A = set0.

Proof.

by rewrite predeqE => t; split => // -[]. Qed.

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

Proof.

by apply/predeqP => x; split=> //= _; apply: lem. Qed.

Lemma : ~` A `|` A = setT

Proof.

by rewrite setUC setUv. Qed.

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

Proof.

by rewrite -setUA setUv setUT. Qed.

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

Proof.

by rewrite setUA setvU setTU. Qed.

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

Proof.

by rewrite -setIA setICr setI0. Qed.

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

Proof.

by rewrite setIA setICl set0I. Qed.

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

Proof.

by rewrite setDE setICA -setDE setDv setI0. Qed.

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

Proof.

by rewrite setIC setDIK. Qed.

Lemma : A a -> a |` A `\ a = A.

Proof.

by move=> Aa; rewrite setDUK//= => x ->. Qed.

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

Proof.

by apply/predeqP => b; case: ifPn; rewrite (inE, notin_setE) => Aa;
split=> [[]|]//; [move=> -> //|move=> /[swap] -> /Aa].
Qed.

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

Proof.

by rewrite setIC setI1. Qed.

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

Proof.

by rewrite eqEsubset propeqE; split=> [A0|[]//]; split. Qed.

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

Proof.

by rewrite eqEsubset propeqE; split=> [|[]]. Qed.

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

Proof.

by apply/propext; split=> [|/[!inE] xA _ ->//]; rewrite inE; exact. Qed.

Lemma : A `<=` setT

Proof.

by []. Qed.

Lemma { } : A = B -> A `<=` B

Proof.

by move->. Qed.

Definition { } : A = B -> B `<=` A := subsetW \o esym.

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

Proof.

by []. Qed.

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

Proof.

exact/eqP. Qed.

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

Proof.

by rewrite subset0; apply: disj_set2P. Qed.

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

Proof.

by rewrite !disj_set2E setIC. Qed.

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

Proof.

apply: (iffP disj_setPS) => [P t ?|P t [/P//]].
by apply: contrapT => ?; apply: (P t).
Qed.

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

Proof.

by rewrite disj_set_sym; apply: disj_setPCl. Qed.

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

Proof.

by apply: (equivP idP); rewrite (rwP disj_setPCl) setCK. Qed.

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

Proof.

by apply: (equivP idP); rewrite (rwP disj_setPCr) setCK. Qed.

Lemma : A `<=` B <-> A `&` ~` B = set0.

Proof.

by rewrite (rwP disj_setPCl) (rwP eqP). Qed.

Lemma : A `&` B = set0 <-> A `<=` ~` B.

Proof.

by rewrite subsets_disjoint setCK. Qed.

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

Proof.

rewrite !inE; apply/propext; split; first by move/[apply]; apply.
by move=> NAx y; apply: contraPnot => ->.
Qed.

Lemma : A `<=` B -> A `\` C `<=` B `\` C.

Proof.

by rewrite !setDE; apply: setSI. Qed.

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

Proof.

by rewrite predeqE => t; split => // -[]. Qed.

Lemma : (A != set0) <-> (A !=set0).

Proof.

split=> [/negP A_neq0|[t tA]]; last by apply/negP => /eqP A0; rewrite A0 in tA.
apply: contrapT => /asboolPn/forallp_asboolPn A0; apply/A_neq0/eqP.
by rewrite eqEsubset; split.
Qed.

Lemma : ~ (A !=set0) <-> A = set0.

Proof.

by split; [|move=> ->]; move/set0P/negP; [move/negbNE/eqP|]. Qed.

Lemma : (T -> False) -> all_equal_to (set0 : set T).

Proof.

by move=> TF A; rewrite -subset0 => x; have := TF x. Qed.

Lemma : A `<=` B -> A !=set0 -> B !=set0.

Proof.

by move=> sAB [x Ax]; exists x; apply: sAB. Qed.

Lemma : A `<=` B -> ~` B `<=` ~` A.

Proof.

by move=> sAB ? nBa ?; apply/nBa/sAB. Qed.

Lemma : ~` A `<=` B -> ~` B `<=` A.

Proof.

by move=> /subsetC; rewrite setCK. Qed.

Lemma : A `<=` ~` B -> B `<=` ~` A.

Proof.

by move=> /subsetC; rewrite setCK. Qed.

Lemma : ~` A `<=` ~` B -> B `<=` A.

Proof.

by move=> /subsetC; rewrite !setCK. Qed.

Lemma : ~` A `<=` ~` B <-> B `<=` A.

Proof.

by split=> /subsetC; rewrite ?setCK. Qed.

Lemma : ~` A `<=` B <-> ~` B `<=` A.

Proof.

by split=> /subsetC; rewrite ?setCK. Qed.

Lemma : A `<=` ~` B <-> B `<=` ~` A.

Proof.

by split=> /subsetC; rewrite ?setCK. Qed.

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

Proof.

by move=> x; left. Qed.

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

Proof.

by move=> x; right. Qed.

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

Proof.

rewrite propeqE; split => [|[BA CA] x]; last by case; [exact: BA | exact: CA].
by move=> sBC_A; split=> x ?; apply sBC_A; [left | right].
Qed.

Lemma : A `&` B = A <-> A `<=` B.

Proof.

rewrite predeqE; split=> [AB t /AB [] //|AB t].
by split=> [[]//|At]; split=> //; exact: AB.
Qed.

Lemma : A `&` B = B <-> B `<=` A.

Proof.

by rewrite setIC setIidPl. Qed.

Lemma : A `<=` B -> A `&` B = A

Proof.

by rewrite setIidPl. Qed.

Lemma : B `<=` A -> A `&` B = B

Proof.

by rewrite setIidPr. Qed.

Lemma : A `|` B = A <-> B `<=` A.

Proof.

split=> [<- ? ?|BA]; first by right.
rewrite predeqE => t; split=> [[//|/BA//]|?]; by left.
Qed.

Lemma : A `|` B = B <-> A `<=` B.

Proof.

by rewrite setUC setUidPl. Qed.

Lemma : B `<=` A -> A `|` B = A

Proof.

by rewrite setUidPl. Qed.

Lemma : A `<=` B -> A `|` B = B

Proof.

by rewrite setUidPr. Qed.

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

Proof.

rewrite propeqE; split=> [H|[y z ??]]; split; by [move=> ?/H[]|apply y|apply z].
Qed.

Lemma : A `\` B = A <-> A `&` B = set0.

Proof.

rewrite setDE disjoints_subset predeqE; split => [AB t|AB t].
by rewrite -AB => -[].
by split=> [[]//|At]; move: (AB t At).
Qed.

Lemma : A `&` B = set0 -> A `\` B = A.

Proof.

by move=> /setDidPl. Qed.

Lemma : A `<=` C \/ B `<=` C -> A `&` B `<=` C.

Proof.

case=> sub a; by [move=> [/sub] | move=> [_ /sub]]. Qed.

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

Proof.

by move=> x []. Qed.

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

Proof.

by move=> x []. Qed.

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

Proof.

by rewrite setDE; apply: subIsetl. Qed.

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

Proof.

by rewrite setDE; apply: subIsetr. Qed.

Lemma :
A `<=` B -> C `<=` D -> A `&` C !=set0 -> B `&` D !=set0.

Proof.

by move=> AB CD [x [/AB Bx /CD Dx]]; exists x. Qed.

Lemma :
A `<=` B -> C `<=` D -> B `&` D = set0 -> A `&` C = set0.

Proof.

by move=> AB /(subsetI_neq0 AB); rewrite -!set0P => /contra_eq. Qed.

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

Proof.

rewrite propeqE; split=> [ADB0 a|sAB].
by apply: contraPP => nBa xA; rewrite -[False]/(set0 a) -ADB0.
by rewrite predeqE => ?; split=> // - [?]; apply; apply: sAB.
Qed.

Lemma : (A `<` B) = (A != B /\ A `<=` B).

Proof.

rewrite /proper andC propeqE; split => [[BA AB]|[/eqP]].
by split => //; apply/negP; apply: contra_not BA => /eqP ->.
by rewrite eqEsubset => AB BA; split => //; exact: contra_not AB.
Qed.

Lemma : ~ (A `<=` B) -> A `&` ~` B !=set0.

Proof.

by rewrite -setD_eq0 setDE -set0P => /eqP. Qed.

Lemma : (A `|` B = set0) = ((A = set0) /\ (B = set0)).

Proof.

by rewrite -!subset0 subUset. Qed.

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

Proof.

rewrite propeqE; split => [|BA].
by move/subsets_disjoint; rewrite setCK setIC => /subsets_disjoint.
by apply/subsets_disjoint; rewrite setCK setIC; apply/subsets_disjoint.
Qed.

Lemma : A `\` setT = set0.

Proof.

by rewrite setDE setCT setI0. Qed.

Lemma : set0 `\` A = set0.

Proof.

by rewrite setDE set0I. Qed.

Lemma : A `\` set0 = A.

Proof.

by rewrite setDE setC0 setIT. Qed.

Lemma : A `<=` B -> C `\` B `<=` C `\` A.

Proof.

by rewrite !setDE -setCS; apply: setIS. Qed.

Lemma : A `<=` C -> D `<=` B -> A `\` B `<=` C `\` D.

Proof.

by move=> /(@setSD B) /subset_trans sAC /(@setDS C) /sAC. Qed.

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

Proof.

rewrite predeqE => z.
by apply: asbool_eq_equiv; rewrite asbool_and !asbool_neg asbool_or negb_or.
Qed.

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

Proof.

by rewrite -[in LHS](setCK A) -[in LHS](setCK B) -setCU setCK. Qed.

Lemma : ~` (A `\` B) = ~` A `|` B.

Proof.

by rewrite setDE setCI setCK. Qed.

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

Proof.

by rewrite !setDE setCU setIIr. Qed.

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

Proof.

move=> A B C; rewrite predeqE => t; split.
by move=> [[At|Bt] Ct]; [left|right].
by move=> [[At Ct]|[Bt Ct]]; split => //; [left|right].
Qed.

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

Proof.

by move=> A B C; rewrite ![A `&` _]setIC setIUl. Qed.

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

Proof.

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

Proof.

by move=> A B C; rewrite ![A `|` _]setUC setUIl. Qed.

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

Proof.

by rewrite eqEsubset; split => [t []//|t ?]; split => //; left. Qed.

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

Proof.

by rewrite eqEsubset; split => [t []//|t ?]; split => //; right. Qed.

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

Proof.

by rewrite eqEsubset; split => [t [[]//|//]|t At]; right. Qed.

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

Proof.

by rewrite eqEsubset; split => [t [//|[]//]|t At]; left. Qed.

Lemma : left_distributive setD (@setU T).

Proof.

by move=> A B C; rewrite !setDE setIUl. Qed.

Lemma : A `&` B `<=` set0 -> (A `|` B) `\` A = B.

Proof.

by move=> AB0; rewrite setDUl setDv set0U setDidl// -subset0 setIC. Qed.

Lemma : A `&` B `<=` set0 -> (B `|` A) `\` A = B.

Proof.

by move=> *; rewrite setUC setUKD. Qed.

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

Proof.

by rewrite !setDE setIA. Qed.

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

Proof.

by rewrite setIC !setIDA setIC. Qed.

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

Proof.

by rewrite 2!setDE setCI setCK setIUr setICr set0U. Qed.

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

Proof.

by rewrite !setDE setCU setIA. Qed.

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

Proof.

by rewrite !setDE setCI setIUr setCK. Qed.

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

Proof.

by rewrite !setDE setCI setIUr. Qed.

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

Proof.

by rewrite setUC -setDDr setDv setD0. Qed.

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

Proof.

apply/seteqP; split=> [x [[Ax|Bx] Cx]|x [[Ax]|[Bx] Cx]].
- by left.
- by right.
- by split=> //; left.
- by split=> //; right.
Qed.

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

Proof.

by rewrite predeqE => -[t u]; split => // -[]. Qed.

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

Proof.

by rewrite predeqE => -[t u]; split => // -[]. Qed.

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

Proof.

exact/predeqP. Qed.

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

Proof.

by rewrite predeqE => -[x y]; split => //= -[]. Qed.

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

Proof.

by rewrite predeqE => -[x y]; split => //= -[]. Qed.

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

Proof.

by rewrite predeqE => -[x y]; split=> [[[? ?] [*]//]|[] [? ?] [*]]. Qed.

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

Proof.

by move=> AB CD x [] /CD Dx1 /AB Bx2. Qed.

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

Proof.

rewrite predeqE => -[x y]; split; first by move=> [/= Ax [n Pn Fny]]; exists n.
by move=> [n Pn [/= Ax Fny]]; split => //; exists n.
Qed.

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

Proof.

rewrite predeqE => -[x y]; split; first by move=> [[n Pn Fnx] Ax]; exists n.
by move=> [n Pn [/= Ax Fny]]; split => //; exists n.
Qed.

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

Proof.

by apply/predeqP => -[i j]; split=> [[? ? [/= -> //]]|[]]; exists i. Qed.

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

Proof.

by apply/predeqP => -[i j]; split=> [[? ? [? /= -> //]]|[]]; exists j. Qed.

Lemma : right_id set0 (@setY T).

Proof.

by move=> A; rewrite /setY setD0 set0D setU0. Qed.

Lemma : left_id set0 (@setY T).

Proof.

by move=> A; rewrite /setY set0D setD0 set0U. Qed.

Lemma : A `+` A = set0.

Proof.

by rewrite /setY setDv setU0. Qed.

Lemma : commutative (@setY T).

Proof.

by move=> A B; rewrite /setY setUC. Qed.

Lemma : A `+` [set: T] = ~` A.

Proof.

by rewrite /setY setDT set0U setTD. Qed.

Lemma : [set: T] `+` A = ~` A.

Proof.

by rewrite setYC setYTC. Qed.

Lemma : associative (@setY T).

Proof.

move=> A B C; rewrite /setY; apply/seteqP; split => x/=;
by have [|] := pselect (A x); have [|] := pselect (B x);
have [|] := pselect (C x); tauto.
Qed.

Lemma : left_distributive (@setI T) (@setY T).

Proof.

move=> A B C; rewrite /setY; apply/seteqP; split => x/=;
by have [|] := pselect (A x); have [|] := pselect (B x);
have [|] := pselect (C x); tauto.
Qed.

Lemma : right_distributive (@setI T) (@setY T).

Proof.

by move=> A B C; rewrite setIC setIYl -2!(setIC A). Qed.

Lemma : A `+` B = (A `\` B) `|` (B `\` A).

Proof.

by []. Qed.

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

Proof.

rewrite /setY; apply/seteqP; split => x/=;
by have [|] := pselect (A x); have [|] := pselect (B x); tauto.
Qed.

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

Proof.

rewrite /setY; apply/seteqP; split => x/=;
by have [|] := pselect (A x); have [|] := pselect (B x); tauto.
Qed.

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

Proof.

rewrite /setY; apply/seteqP; split => x/=;
by have [|] := pselect (A x); have [|] := pselect (B x); tauto.
Qed.

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

Proof.

by rewrite /setY; apply/seteqP; split => x/=; tauto. Qed.

Lemma : A `+` ~` A = [set: T].

Proof.

by rewrite /setY setDE setCK setIid setDE setIid setUv. Qed.

Lemma : ~` A `+` A = [set: T].

Proof.

by rewrite setYC setYCT. Qed.

Lemma : ~ A a -> A `\ a = A.

Proof.

by move=> NDr; apply/setDidPl/disjoints_subset/subsetCr => _ ->. Qed.

End basic_lemmas.
Arguments subsetT {T} A.

#[global]
Hint Resolve subsetUl subsetUr subIsetl subIsetr subDsetl subDsetr : core.
Arguments setU_id2r {T} C {A B}.

Lemma { } ( : T) ( : set I) :
[set x | _ in A] = if A == set0 then set0 else [set x].

Proof.

apply/seteqP; split=> [_ [i +] <-|t]; first by case: ifPn => // /eqP ->.
by case: ifPn => // /set0P[i Ai ->{t}]; exists i.
Qed.

Section set_order.
Import Order.TTheory.

Lemma ( : porderType d) ( : T -> rT) :
[set | f x = g x] = [set | (f x <= g x)%O] `&` [set | (f x >= g x)%O].

Proof.

by apply/seteqP; split => [x/= ->//|x /andP]; rewrite -eq_le =>/eqP. Qed.

Lemma ( : orderType d) ( : T -> rT) :
[set | f x != g x ] = [set | (f x < g x)%O] `|` [set | (f x > g x)%O].

Proof.

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

End set_order.

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

Proof.

apply/predeqP => x; split=> [[a ? [b ? <-]]|[[a b] [? ? <-]]]/=;
by [exists (a, b) | exists a => //; exists b].
Qed.

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

Proof.

by rewrite predeqP. Qed.

Lemma ( : eqType) ( : T) : [set` [:: x]] = [set x].

Proof.

by apply/seteqP; split => y /=; rewrite ?inE => /eqP. Qed.

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

Proof.

apply/eqP/eqP=> [|->]; rewrite predeqE //; case: S => // h t /(_ h).
by rewrite /= mem_head => -[/(_ erefl)].
Qed.

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

Proof.

by rewrite set_seq_eq0. Qed.

Section InitialSegment.

Lemma : `I_0 = set0

Proof.

by rewrite predeqE. Qed.

Lemma : `I_1 = [set 0]

Proof.

by rewrite predeqE; case. Qed.

Lemma : `I_n = set0 -> n = 0.

Proof.

by case: n => // n; rewrite predeqE; case/(_ 0%N); case. Qed.

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

Proof.

rewrite /mkset predeqE => i; split => [|[|->//]].
by rewrite ltnS leq_eqVlt => /orP[/eqP ->|]; by [left|right].
by move/ltn_trans; apply.
Qed.

Lemma : `I_n.+1 = n |` `I_n.

Proof.

by rewrite setUC IIS. Qed.

Lemma : `I_n.+1 `\ n = `I_n.

Proof.

by rewrite IIS setUDK// => x [->/=]; rewrite ltnn. Qed.

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

Proof.

by (case: leqP => mn; [rewrite setIidl// | rewrite setIidr//])
=> k /= /leq_trans; apply => //; apply: ltnW.
Qed.

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

Proof.

by (case: leqP => mn; [rewrite setUidr// | rewrite setUidl//])
=> k /= /leq_trans; apply => //; apply: ltnW.
Qed.

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

Proof.

by apply/seteqP; split => [|] ?; rewrite /= mem_iota add0n. Qed.

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

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

Proof.

by move=> k; apply/val_inj. Qed.

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

Proof.

by move=> k; apply/val_inj. Qed.

Lemma : ~` `I_n = [set | n <= k].

Proof.

by apply/seteqP; split => [x /negP|x /= nx]; last apply/negP; rewrite -leqNgt.
Qed.

Lemma : (n \in ~` `I_N) = (N <= n).

Proof.

by rewrite in_setC /mkset /in_mem /mem /= /in_set asboolb -leqNgt. Qed.

End InitialSegment.

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

Proof.

by apply/seteqP; split => // -[]. Qed.

Lemma ( : set unit) : A = set0 \/ A = setT.

Proof.

have [->|/set0P[[] Att]] := eqVneq A set0; [by left|right].
by apply/seteqP; split => [|] [].
Qed.

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

Proof.

by rewrite eqEsubset; split => // [[]] // _; [left|right]. Qed.

Lemma ( : set bool) :
[\/ B == [set true], B == [set false], B == set0 | B == setT].

Proof.

have [Bt|Bt] := boolP (true \in B); have [Bf|Bf] := boolP (false \in B).
- have -> : B = setT by apply/seteqP; split => // -[] _; exact: set_mem.
  by apply/or4P; rewrite eqxx/= !orbT.
- suff : B = [set true] by move=> ->; apply/or4P; rewrite eqxx.
  apply/seteqP; split => -[]// /mem_set; last by move=> _; exact: set_mem.
  by rewrite (negbTE Bf).
- suff : B = [set false] by move=> ->; apply/or4P; rewrite eqxx/= orbT.
  apply/seteqP; split => -[]// /mem_set; last by move=> _; exact: set_mem.
  by rewrite (negbTE Bt).
- suff : B = set0 by move=> ->; apply/or4P; rewrite eqxx/= !orbT.
  by apply/seteqP; split => -[]//=; rewrite 2!notin_setE in Bt, Bf.
Qed.

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

Proof.

rewrite -fsetI_eq0; apply/idP/idP; apply: contraLR.
by move=> /set0P[t [tA tB]]; apply/fset0Pn; exists t; rewrite inE; apply/andP.
by move=> /fset0Pn[t]; rewrite inE => /andP[tA tB]; apply/set0P; exists t.
Qed.

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

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

Proof.

by rewrite -subset0 => x. Qed.

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

Proof.

by rewrite predeqE => y; split; rewrite /= inE => /eqP. Qed.

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

Proof.

by rewrite predeqE => x; split; rewrite /= !inE; [case/andP|case=> -> ->].
Qed.

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

Proof.

by apply/predeqP => x /=; split; rewrite 2!inE/= => /andP. Qed.

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

Proof.

rewrite predeqE => x; split; rewrite /= !inE.
by case/orP; [left|right].
by move=> []->; rewrite ?orbT.
Qed.

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

Proof.

by rewrite set_fsetU set_fset1. Qed.

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

Proof.

rewrite predeqE => x; split; rewrite /= !inE; last by move=> [-> /negP ->].
by case/andP => /negP xNB xA.
Qed.

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

Proof.

by rewrite set_fsetD set_fset1. Qed.

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

Proof.

apply/predeqP => x; split=> [/imfsetP[i ip -> /=]|]; first by exists i.
by move=> [i ip <-]; apply: in_imfset.
Qed.

End SetFset.

Section SetMonoids.
Variable ( : Type).

Import Monoid.
..Build (set T) set0 setU setUA setUC set0U.
..Build (set T) setT setU setTU setUT.
..Build (set T) setT setI setIA setIC setTI.
..Build (set T) set0 setI set0I setI0.
..Build (set T) setU setI setUIl setUIr.
..Build (set T) setI setU setIUl setIUr.

..Build (set T) set0 setY setYA setYC set0Y.
..Build (set T) setI setY setIYl setIYr.

End SetMonoids.

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

Lemma : A a -> (f @` A) (f a)

Proof.

by exists a. Qed.

Lemma : a \in A -> f a \in [set f x | in A].

Proof.

by rewrite !inE; apply/imageP. Qed.

Lemma ( : aT -> rT) ( : aT) : range f (f a).

Proof.

by apply: imageP. Qed.

Lemma : f a \in range f.

Proof.

by rewrite !inE; apply/imageT. Qed.

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 { : Type}.
Implicit Types (A B : set aT) (f : aT -> rT) (Y : set rT).

Lemma { } : injective f -> (f @` A) (f a) = A a.

Proof.

by move=> f_inj; rewrite propeqE; split => [[b Ab /f_inj <-]|/(imageP f)//].
Qed.

Lemma { } : injective f ->
(f a \in [set f x | in A]) = (a \in A).

Proof.

by move=> /image_inj finj; apply/idP/idP; rewrite !inE finj. Qed.

Lemma : id @` A = A.

Proof.

by rewrite eqEsubset; split => a; [case=> /= x Ax <-|exists a]. Qed.

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

Proof.

by split=> fAY x; have := fAY x; rewrite !inE. Qed.

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

Proof.

by split=> fAY x => [Ax|[y + <-]]; apply: fAY=> //; exists x. Qed.

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

Proof.

by apply/propext; rewrite image_subP; split=> AB a /AB. Qed.

Lemma : f @` A `<=` [set x] -> forall , A a -> f a = x.

Proof.

by move=> + a Aa; apply; exists a. Qed.

Lemma : f @` A `<=` [set x] <-> forall , A a -> f a = x.

Proof.

by split=> [/(@imsub1 _)//|+ _ [a Aa <-]]; apply. Qed.

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

Proof.

rewrite eqEsubset; split => b.
- by case=> a [] Ha <-; [left | right]; apply imageP.
- by case=> -[] a Ha <-; apply imageP; [left | right].
Qed.

Lemma : f @` set0 = set0.

Proof.

by rewrite eqEsubset; split => b // -[]. Qed.

Lemma : f @` A = set0 -> A = set0.

Proof.

move=> fA0; rewrite predeqE => t; split => // At.
by have : set0 (f t) by rewrite -fA0; exists t.
Qed.

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

Proof.

by rewrite eqEsubset; split => [b [a' -> <-] //|b ->]; exact/imageP. Qed.

Lemma : A `<=` [set a] -> A = set0 \/ A = [set a].

Proof.

move=> Aa; have [/eqP|/set0P[t At]] := boolP (A == set0); first by left.
by right; rewrite eqEsubset; split => // ? ->; rewrite -(Aa _ At).
Qed.

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

Proof.

have [<-|ab Aab] := pselect (a = b).
  by rewrite setUid => /subset_set1[]->; [apply: Or41|apply: Or42].
have [|/nonsubset[x [/[dup] /Aab []// -> Ab _]]] := pselect (A `<=` [set a]).
  by move=> /subset_set1[]->; [apply: Or41|apply: Or42].
have [|/nonsubset[y [/[dup] /Aab []// -> Aa _]]] := pselect (A `<=` [set b]).
  by move=> /subset_set1[]->; [apply: Or41|apply: Or43].
by apply: Or44; apply/seteqP; split=> // z /= [] ->.
Qed.

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

Proof.

by move=> b [x [Aa Ba <-]]; split; apply: imageP. Qed.

Lemma : f @` A !=set0 -> A !=set0.

Proof.

by case=> b [a]; exists a. Qed.

Lemma : A !=set0 -> f @` A !=set0.

Proof.

by move=> [x] Ax; exists (f x), x. Qed.

Lemma : A `<=` B -> f @` A `<=` f @` B.

Proof.

by move=> AB _ [a Aa <-]; exists a => //; apply/AB. Qed.

Lemma : f @^-1` set0 = set0

Proof.

exact/predeqP. Qed.

Lemma : f @^-1` setT = setT

Proof.

by []. Qed.

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

Proof.

by case=> [t ?]; exists (f t). Qed.

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

Proof.

by move=> a Aa; exists a. Qed.

Lemma : f @^-1` (range f) = [set: aT].

Proof.

by rewrite eqEsubset; split=> x // _; exists x. Qed.

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

Proof.

by move=> _ [t /= Yft <-]. Qed.

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

Proof.

move=> fsurj; rewrite predeqE => x; split; first by move=> [? ? <-].
move=> Yx; have : setT x by [].
by rewrite -fsurj => - [y _ fy_eqx]; exists y => //=; rewrite fy_eqx.
Qed.

Lemma ( : set T1) ( : T1 -> T2) :
(forall , A x -> f x = f' x) -> f @` A = f' @` A.

Proof.

by move=> h; rewrite predeqE=> y; split=> [][x ? <-]; exists x=> //; rewrite h.
Qed.

Lemma : (forall , A x -> g x = x) -> g @` A = A.

Proof.

by move=> /eq_imagel->; rewrite image_id. Qed.

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

Proof.

exact/predeqP. Qed.

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

Proof.

exact/predeqP. Qed.

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

Proof.

by rewrite predeqE => a; split=> nAfa ?; apply: nAfa. Qed.

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

Proof.

by move=> Y12 t /Y12. Qed.

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

Proof.

by split; case=> t ?; exists t. Qed.

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

Proof.

exact/predeqP. Qed.

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

Proof.

exact/predeqP. Qed.

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

Proof.

move=> eqFG; apply/predeqP => i.
by split=> [] [Di FAi]; split; rewrite /preimage//= (eqFG,=^~eqFG) ?inE.
Qed.

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

Proof.

by rewrite notin_setE/=; apply: contra_notP => /eqP/set0P[t [Dt fit]]; exists t.
Qed.

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

Proof.

by []. Qed.

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

Proof.

by []. Qed.

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

Proof.

rewrite predeqE => t; split => /=.
by move=> -[r Cr <-]; rewrite inE; exists r.
by rewrite inE => -[r Cr <-]; exists r.
Qed.

Lemma ( : aT -> rT) ( : set rT) :
f @^-1` (Y1 `&` Y2) = set0 <-> f @^-1` Y1 `&` f @^-1` Y2 = set0.

Proof.

by split; apply: contraPP => /eqP/set0P/(nonempty_preimage_setI f _ _).2/set0P/eqP.
Qed.

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

Proof.

by move=> ->; rewrite preimage_set0. Qed.

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

Proof.

by rewrite -subset0 => + x /= Afx => /(_ (f x))[]; split. Qed.

Lemma { } { : T -> R} {} : ~ range f x <-> f @^-1` [set x] = set0.

Proof.

split => [fx|]; first by rewrite preimage0// => ? [->].
by apply: contraPnot => -[t _ <-] /seteqP[+ _] => /(_ t) /=.
Qed.

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

Proof.

by move/preimage10P. Qed.

Lemma {} ( : {pred T}) : P @^-1` [set true] = [set` P].

Proof.

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

Lemma {} ( : {pred T}) : P @^-1` [set false] = ~` [set` P].

Proof.

by apply/seteqP; split => [t/= /negbT/negP|t /= /negP/negbTE]. Qed.

Lemma {} ( : set T) : mem A @^-1` [set true] = A.

Proof.

by rewrite preimage_true; under eq_fun do rewrite inE. Qed.

Lemma {} ( : set T) : mem A @^-1` [set false] = ~` A.

Proof.

by rewrite preimage_false; under eq_fun do rewrite inE. Qed.

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

Lemma { : Type} ( : aT -> bT -> rT)
( : set aT) ( : set bT) : A `<=` B -> C `<=` D ->
[set f x y | in A & in C] `<=` [set f x y | in B & in D].

Proof.

by move=> AB CD; rewrite !image2E; apply: image_subset; exact: setSX. Qed.

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

Proof.

by rewrite eqEsubset; split => [x [b [a Aa] <- <-]|x [a Aa] <-];
[apply/imageP |apply/imageP/imageP].
Qed.

Definition := set (set U).
Identity Coercion set_system_to_set : set_system >-> set.

Section set_systems.
Context {} ( : set_system T).

Definition := forall , G A -> G B -> G (A `&` B).

Definition := forall , G A -> G B -> G (A `|` B).

End set_systems.

Lemma ( : set_system T) :
setI_closed F -> setI_closed (F `|` [set setT]).

Proof.

move=> IF=> C D [FC|/= ->{C}].
- by move=> [FD|/= ->{D}]; [left; exact: IF|rewrite setIT; left].
- by move=> [FD|->{D}]; [rewrite setTI; left|rewrite !setTI; right].
Qed.

Lemma ( : set_system T) :
setI_closed F -> setI_closed (F `|` [set set0]).

Proof.

move=> IF=> C D [FC|/= ->{C}].
- by move=> [FD|/= ->{D}]; [left; exact: IF|rewrite setI0; right].
- by move=> [FD|->{D}]; [rewrite set0I; right|rewrite !set0I; right].
Qed.

Section rectangle.
Context { : Type}.
Implicit Types (X : set_system T1) (Y : set_system T2).

Definition : set_system (T1 * T2) :=
[set U `*` V | in X & in Y].

Lemma : X A -> Y B -> rectangle X Y (A `*` B).

Proof.

by move=> XA YB; exists A => //; exists B. Qed.

Lemma : setI_closed X -> setI_closed Y ->
setI_closed (rectangle X Y).

Proof.

move=> IG IH _ _ [A mA [B mB] <-] [A' mA' [B' mB'] <-].
by rewrite -setXI; apply: rectangle_setX; [exact: IG|exact: IH].
Qed.

End rectangle.

Definition { : Type} ( : set aT) ( : aT -> rT)
    ( : set_system rT) : set_system aT :=
  [set D `&` f @^-1` B | in G].

Lemma { : Type} ( : set aT) ( : aT -> rT) :
  preimage_set_system D f set0 = set0.

Proof.

exact: image_set0. Qed.

Lemma { : Type} ( : set aT) ( : aT -> rT) :
{morph preimage_set_system D f : / x `|` y >-> x `|` y}.

Proof.

exact: image_setU. Qed.

Lemma { : Type} ( : set aT)
    ( : aT -> bT) ( : bT -> rT) ( : set_system rT) :
  preimage_set_system D (g \o f) F
    = preimage_set_system D f (preimage_set_system setT g F).

Proof.

apply/seteqP; split=> [_ [B FB] <-|_ [_ [C FC <-] <-]].
by exists (g @^-1` B) => //; exists B => //; rewrite setTI.
by exists C => //; rewrite setTI comp_preimage.
Qed.

Lemma { : Type} ( : set aT) ( : set_system aT) :
preimage_set_system D idfun F = setI D @` F.

Proof.

by []. Qed.

Lemma { } ( : set_system T2) ( : T1 -> T2) :
A `<=` B ->
preimage_set_system [set: _] f A `<=` preimage_set_system [set: _] f B.

Proof.

by move=> AB _ [C ? <-]; exists C => //; exact: AB. Qed.

Definition ( : Type) ( : set aT) ( : aT -> rT)
    ( : set_system aT) : set_system rT :=
  [set : set rT | G (D `&` f @^-1` B)].

Section cross.
Context { : Type}.
Implicit Types (X : set_system T1) (Y : set_system T2).

Definition ( : T -> T1) ( : T -> T2) :=
  preimage_set_system [set: T] f X
  `|` preimage_set_system [set: T] g Y.

End cross.

Definition { : Type} := @cross (T1 * T2)%type T1 T2 fst snd.
Notation := (cross12 A B) : classical_set_scope.

Notation := [set (x + y)%R | in A & in B].

Section addsetTheory.
Context { : zmodType}.
Import GRing.Theory.
Local Open Scope ring_scope.
Implicit Types A B C D : set E.

Lemma : A `<=` B -> C `<=` D -> A `+ C `<=` B `+ D.

Proof.

by move=> AB CD z [a /AB Ba [c /CD Dc <-]]; exists a => //; exists c.
Qed.

Lemma : [set 0] `+ A = A.

Proof.

apply/seteqP; split => z /=.
by move=> [+ -> [y]]; rewrite add0r => + + <-.
by move=> Az; exists 0 => //; exists z; rewrite ?add0r.
Qed.

Lemma ( : E) :
[set x] `+ (A `&` B) = ([set x] `+ A) `&` ([set x] `+ B).

Proof.

apply/seteqP; split => z.
  by move => [r Cr] [y [Ay By] <- {z}]; split => /=; exists r => //;
    exists y.
move=> /= [[r ->] [y Ay] <- {z}] [x' ->] [y' By'] /(congr1 (fun => h - x)).
rewrite addrAC subrr add0r addrAC subrr add0r => yy'.
move: By'; rewrite yy' {y' yy'} => By.
by exists x => //;  exists y.
Qed.

Lemma : [set x + y] `+ A `<=` [set x] `+ ([set y] `+ A).

Proof.

move=> _/= [_ ->] [z Az <-]; exists x => //; exists (y + z); last exact: addrA.
by exists y => //; exists z.
Qed.

End addsetTheory.

Lemma { } { : set_system T'} ( : T -> T') ( : T' -> T) :
cancel f g -> [set | P (f @` A)] `<=` [set g @` A | in P].

Proof.

by move=> ? A; exists (f @` A); rewrite ?image_comp ?eq_image_id/=. Qed.

Lemma ( : set_system T') ( : T -> T') ( : T' -> T) :
cancel g f -> [set g @` A | in P] `<=` [set | P (f @` A)].

Proof.

by move=> gK _ [B /= ? <-]; rewrite image_comp eq_image_id/=. Qed.

Lemma { } { : set_system T'} ( : T -> T') ( : T' -> T) :
cancel f g -> cancel g f ->
[set g @` A | in P] = [set | P (f @` A)].

Proof.

by move=> fK gK; apply/seteqP; split; [apply: subimageK | apply: subKimage].
Qed.

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

Proof.

by rewrite -subset0 => x []. Qed.

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

Proof.

by apply/seteqP; split=> [_ [_ -> <-]|_ ->]//=; exists x. Qed.

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

Proof.

apply/seteqP; split; first by move=> _ [x nAx <-]; split=> // -[y /[swap]-[->]].
by move=> [x [_ exAx]|[/(_ erefl)//]]; exists x => // Ax; apply: exAx; exists x.
Qed.

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

Proof.

by rewrite -[setT]setCK some_setC setCT some_set0 setD0. Qed.

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

Proof.

apply/seteqP; split; first by move=> _ [x [Ax Bx] <-]; split; exists x.
by move=> _ [[x + <-] [y By []]] => /[swap]<- Ay; exists y.
Qed.

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

Proof.

by rewrite -[_ `|` _]setCK setCU some_setC some_setI setDIr -!some_setC !setCK.
Qed.

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

Proof.

by rewrite some_setI some_setC setIDA setIidl// => _ [? _ <-]. Qed.

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

Proof.

by move=> + x Ax => /(_ (Some x))[|y By [<-]]; first by exists x. Qed.

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

Proof.

by split=> [/sub_image_some//|/image_subset]. Qed.

Lemma {} ( : set T) : some @` A = some @` B -> A = B.

Proof.

by move=> e; apply/seteqP; split; apply: sub_image_some; rewrite e. Qed.

Lemma {} ( : set T) : some @` A = set0 <-> A = set0.

Proof.

split=> [|->]; last by rewrite some_set0.
by rewrite -!subset0 => A0 x Ax; apply: (A0 (some x)); exists x.
Qed.

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

Proof.

apply/seteqP; split; first by move=> _ [a Afa <-]; exists (f a).
by move=> [x|] [a Aa //= [afx]]; exists x; rewrite // -afx.
Qed.

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

Proof.

by rewrite !image_comp. Qed.

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

Proof.

by apply/disj_setPS/disj_setPS; rewrite -some_setI -some_set0 sub_image_someP.
Qed.

Lemma ( : A) ( : set B) :
(inl x \in [set inr y | in Y]) = false.

Proof.

by apply/negP; rewrite inE/= => -[]. Qed.

Lemma ( : B) ( : set A) :
(inr y \in [set inl x | in X]) = false.

Proof.

by apply/negP; rewrite inE/= => -[]. Qed.

Lemma ( : B) ( : set B) :
(inr y \in [set @inr A B y | in Y]) = (y \in Y).

Proof.

by apply/idP/idP => [/[!inE][/= [x ? [<-]]]|/[!inE]]//; exists y. Qed.

Lemma ( : A) ( : set A) :
(inl x \in [set @inl A B x | in X]) = (x \in X).

Proof.

by apply/idP/idP => [/[!inE][/= [y ? [<-]]]|/[!inE]]//; exists x. Qed.

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

Lemma : P i -> F i `<=` \bigcup_( in P) F j.

Proof.

by move=> Pi a Fia; exists i. Qed.

Lemma : P i -> \bigcap_( in P) F j `<=` F i.

Proof.

by move=> Pi a /(_ i); apply. Qed.

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

Proof.

move=> F G FG t [i Pi Fit]; have := FG (F i).
by move=> /(_ (ex_intro2 _ _ _ Pi erefl))[j Pj ji]; exists j => //; rewrite ji.
Qed.

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

Proof.

by move=> F G FG t Gt i Pi; have [|j Pj <-] := FG (F i); [exists i|apply: Gt].
Qed.

Lemma : (forall , P i -> F i = G i) ->
\bigcup_( in P) F i = \bigcup_( in P) G i.

Proof.

by move=> FG; rewrite eqEsubset; split; apply: subset_bigcup_r;
move=> A [i ? <-]; exists i => //; rewrite FG.
Qed.

Lemma : (forall , P i -> F i = G i) ->
\bigcap_( in P) F i = \bigcap_( in P) G i.

Proof.

by move=> FG; rewrite eqEsubset; split; apply: subset_bigcap_r;
move=> A [i ? <-]; exists i => //; rewrite FG.
Qed.

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

Proof.

by rewrite eqEsubset; split => [t PFt i Pi ?|t PFt [i Pi ?]];
[apply PFt; exists i | exact: (PFt _ Pi)].
Qed.

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

Proof.

apply: setC_inj; rewrite setC_bigcup setCK.
by apply: eq_bigcapr => ?; rewrite setCK.
Qed.

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

Proof.

apply/seteqP; split=> [_/= [x [i Pi Fix <-]]|]; first by exists i.
by move=> _ [i Pi [x Fix <-]]; exists x => //; exists i.
Qed.

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

Proof.

apply/seteqP; split.
by move=> _ [x Fx <-]; split=> // i; exists x => //; apply: Fx.
by move=> [x|[//=]] [_ Fx]; exists x => //= i /Fx [y ? [<-]].
Qed.

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

Proof.

rewrite predeqE => x; split; last by move=> [[i/= /set_mem Pi] _ Fix]; exists i.
by move=> [i Pi Fix]; exists (SigSub (mem_set Pi)).
Qed.

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

Proof.

by move=> /seteqP->. Qed.

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

Proof.

by move=> /seteqP->. Qed.

Lemma : P `<=>` Q -> (forall , P i -> F i = G i) ->
\bigcup_( in P) F i = \bigcup_( in Q) G i.

Proof.

by move=> /eq_bigcupl<- /eq_bigcupr->. Qed.

Lemma : P `<=>` Q -> (forall , P i -> F i = G i) ->
\bigcap_( in P) F i = \bigcap_( in Q) G i.

Proof.

by move=> /eq_bigcapl<- /eq_bigcapr->. Qed.

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

Proof.

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

Proof.

apply: setC_inj; rewrite !(setCI, setC_bigcap) -bigcupU.
by apply: eq_bigcupr => *; rewrite setCI.
Qed.

Lemma : P !=set0 -> \bigcup_(_ in P) A = A.

Proof.

by case=> j ?; rewrite predeqE => x; split=> [[i //]|Ax]; exists j. Qed.

Lemma : P !=set0 -> \bigcap_(_ in P) A = A.

Proof.

by move=> PN0; apply: setC_inj; rewrite setC_bigcap bigcup_const. Qed.

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

Proof.

by move=> PN0; rewrite bigcapI bigcap_const. Qed.

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

Proof.

by move=> PN0; rewrite bigcapI bigcap_const. Qed.

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

Proof.

by move=> PN0; rewrite bigcupU bigcup_const. Qed.

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

Proof.

by move=> PN0; rewrite bigcupU bigcup_const. Qed.

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

Proof.

by rewrite eqEsubset; split => a // []. Qed.

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

Proof.

by rewrite eqEsubset; split => ? => [[] ? -> //|]; exists i. Qed.

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

Proof.

by rewrite eqEsubset; split=> a // []. Qed.

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

Proof.

by rewrite eqEsubset; split => ?; [exact|move=> ? ? ->]. Qed.

Lemma :
(\bigcup_( in P) F i !=set0) <-> exists2 , P i & F i !=set0.

Proof.

split=> [[t [i ? ?]]|[j ? [t ?]]]; by [exists i => //; exists t| exists t, j].
Qed.

Lemma :
(forall , P i -> F i = set0) -> \bigcup_( in P) F i = set0.

Proof.

by move=> PF; rewrite -subset0 => t -[i /PF ->]. Qed.

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

Proof.

by move=> [i Pi]; rewrite -!subset0 => Fi t Ft; apply/Fi/Ft. Qed.

Lemma :
(forall , P i -> F i = setT) -> \bigcap_( in P) F i = setT.

Proof.

by move=> PF; rewrite -subTset => t -[i /PF ->]. Qed.

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

Proof.

by move=> [i Pi F0]; rewrite -subTset => t; exists i; rewrite ?F0. Qed.

Lemma :
(\bigcup_( in P) F i = set0) <-> forall , P i -> F i = set0.

Proof.

split=> [|/bigcup0//]; rewrite -subset0 => F0 i Pi; rewrite -subset0.
by move=> t Ft; apply: F0; exists i.
Qed.

Lemma :
(\bigcap_( in P) F i = setT) <-> forall , P i -> F i = setT.

Proof.

split=> [|/bigcapT//]; rewrite -subTset => FT i Pi; rewrite -subTset.
by move=> t _; apply: FT.
Qed.

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

Proof.

rewrite predeqE => t; split => [[At [k ? ?]]|[k ? [At ?]]];
by [exists k |split => //; exists k].
Qed.

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

Proof.

by rewrite setIC setI_bigcupr//; under eq_bigcupr do rewrite setIC. Qed.

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

Proof.

apply: setC_inj; rewrite setCU !setC_bigcap setI_bigcupr.
by under eq_bigcupr do rewrite -setCU.
Qed.

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

Proof.

by rewrite setUC setU_bigcapr//; under eq_bigcapr do rewrite setUC. Qed.

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

Proof.

rewrite predeqE => x; split=> [[i Pi Fix]|[i _]].
by exists i => //; case: ifPn; rewrite (inE, notin_setE).
by case: ifPn; rewrite (inE, notin_setE) => Pi Fix; exists i.
Qed.

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

Proof.

rewrite bigcup_mkcond [RHS]bigcup_mkcond; apply: eq_bigcupr => i _.
by rewrite in_setI; case: (i \in P) (i \in Q) => [] [].
Qed.

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

Proof.

rewrite bigcup_mkcond [RHS]bigcup_mkcond; apply: eq_bigcupr => i _.
by rewrite in_setI; case: (i \in P) (i \in Q) => [] [].
Qed.

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

Proof.

apply: setC_inj; rewrite !setC_bigcap bigcup_mkcond; apply: eq_bigcupr => i _.
by case: ifP; rewrite ?setCT.
Qed.

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

Proof.

rewrite bigcap_mkcond [RHS]bigcap_mkcond; apply: eq_bigcapr => i _.
by rewrite in_setI; case: (i \in P) (i \in Q) => [] [].
Qed.

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

Proof.

rewrite bigcap_mkcond [RHS]bigcap_mkcond; apply: eq_bigcapr => i _.
by rewrite in_setI; case: (i \in P) (i \in Q) => [] [].
Qed.

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

Proof.

by rewrite eqEsubset; split=>[a [i ?]->| a [i ?]<-]; [apply: imageP | exists i].
Qed.

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

Proof.

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

Proof.

by apply: setC_inj; rewrite !(setCI, setC_bigcap) bigcup_setU. Qed.

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

Proof.

by rewrite bigcup_setU bigcup_set1. Qed.

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

Proof.

by rewrite bigcap_setU bigcap_set1. Qed.

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

Proof.

by move=> Xx; rewrite -bigcup_setU1 setD1K. Qed.

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

Proof.

by move=> Xx; rewrite -bigcap_setU1 setD1K. Qed.

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

Proof.

by elim/big_rec2: _ => [|i X Y Pi <-]; rewrite ?setC0 ?setCU. Qed.

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

Proof.

by elim/big_rec2: _ => [|i X Y Pi <-]; rewrite ?setCT ?setCI. Qed.

#[deprecated(since="mathcomp-analysis 1.17.0", note="use `setD_bigcupr` instead")]
Lemma ( : I -> set T) ( : set I) ( : set T) : P !=set0 ->
\bigcap_( in P) (A `\` F i) = A `\` \bigcup_( in P) F i.

Proof.

by move=> PN0; rewrite setDE setC_bigcup -bigcapIr. Qed.

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

Proof.

by move=> PN0; rewrite setDE setC_bigcup -bigcapIr. Qed.

Lemma ( : I -> set T) [ : set I] ( : set T) :
A `\` \bigcap_( in P) F i = \bigcup_( in P) (A `\` F i).

Proof.

by rewrite setDE setC_bigcap setI_bigcupr. Qed.

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

Proof.

by rewrite setDE setI_bigcupl; under eq_bigcupr do rewrite -setDE. Qed.

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

Proof.

apply/predeqP => x; split=> [|[i Pi [j Pj Fijx]]]; last by exists (i, j).
by move=> [[/= i j] [Pi Qj] Fijx]; exists i => //; exists j.
Qed.

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

Proof.

exact: bigcup_setX_dep. Qed.

Lemma ( : I -> set T) ( : set I) ( : T -> set T') :
\bigcup_( in \bigcup_( in P) F n) G i =
\bigcup_( in P) \bigcup_( in F n) G i.

Proof.

apply/seteqP; split; first by move=> x [n [m ? ?] h]; exists m => //; exists n.
by move=> x [n ? [m ?]] h; exists m => //; exists n.
Qed.

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

Proof.

by rewrite -bigcup_setU -setIUr setUv setIT. Qed.

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

Proof.

by rewrite -bigcap_setU -setIUr setUv setIT. Qed.

Lemma :
(forall , P i -> F i `<=` A) -> \bigcup_( in P) F i `<=` A.

Proof.

by move=> FD t [n An Fnt]; exact: (FD n). Qed.

Lemma :
(forall , P i -> A `<=` F i) -> A `<=` \bigcap_( in P) F i.

Proof.

by move=> AF t At n Pn; exact: AF. Qed.

Lemma : (forall , P i -> F i `<=` G i) ->
\bigcup_( in P) F i `<=` \bigcup_( in P) G i.

Proof.

by move=> FG; apply: bigcup_sub => i Pi + /(FG _ Pi); apply: bigcup_sup.
Qed.

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

Proof.

by move=> PQ t [i /PQ Qi Fit]; exists i. Qed.

Lemma : (forall , P i -> F i `<=` G i) ->
\bigcap_( in P) F i `<=` \bigcap_( in P) G i.

Proof.

move=> FG; apply: sub_bigcap => i Pi x Fx; apply: FG => //.
exact: bigcap_inf Fx.
Qed.

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

Lemma {} ( : eqType) ( : I -> set T) ( : set I) ( : I) : P j ->
F j `\` \bigcup_( in [set | P k /\ k != j]) (F j `\` F i) =
\bigcap_( in P) F i.

Proof.

move=> Pj; apply/seteqP; split => [t [Fjt UFt] i Pi|t UFt].
by have [->//|ij] := eqVneq i j; apply: contra_notP UFt => Fit; exists i.
by split=> [|[k [Pk kj]] [Fjt]]; [|apply]; exact: UFt.
Qed.

Definition := nat -> R.

Notation := (sequence R) : type_scope.

Definition ( : set T) : (set T)^nat :=
fun => if i == 0 then A else if i == 1 then B else set0.
Arguments bigcup2 T A B n /.

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

Proof.

Lemma ( : set T) : \bigcup_( < 2) (bigcup2 A B) i = A `|` B.

Proof.

Definition ( : set T) : (set T)^nat :=
fun => if i == 0 then A else if i == 1 then B else setT.
Arguments bigcap2 T A B n /.

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

Proof.

apply: setC_inj; rewrite setC_bigcap setCI -bigcup2E /bigcap2 /bigcup2.
by apply: eq_bigcupr => -[|[|[]]]//=; rewrite setCT.
Qed.

Lemma ( : set T) : \bigcap_( < 2) (bigcap2 A B) i = A `&` B.

Proof.

apply: setC_inj; rewrite setC_bigcap setCI -bigcup2inE /bigcap2 /bigcup2.
by apply: eq_bigcupr => // -[|[|[]]].
Qed.

Lemma ( : (set T)^nat) :
\bigcup_ F n = F 0%N `|` \bigcup_( in ~` `I_1) F n.

Proof.

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

Proof.

rewrite eqEsubset; split=> x; first by case=> j [] i pi <- Xfix; exists i.
by case=> i Pi Ffix; exists (f i); [exists i|].
Qed.

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

Proof.

by apply: setC_inj; rewrite !setC_bigcap bigcup_set_type. Qed.

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

Proof.

by apply: setC_inj; rewrite !setC_bigcap bigcup_image. Qed.

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

Proof.

elim/finSet_rect: X => X IHX; have [->|[x xX]] := fset_0Vmem X.
by rewrite big_seq_fset0 -subset0 => x [].
rewrite -(fsetD1K xX) set_fsetU set_fset1 big_fsetU1 ?inE ?eqxx//=.
by rewrite bigcup_setU1 IHX// fproperD1.
Qed.

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

Proof.

by apply: setC_inj; rewrite setC_bigcap setC_bigsetI bigcup_fset. Qed.

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

Proof.

by rewrite set_fsetU1 bigcup_setU1. Qed.

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

Proof.

by rewrite set_fsetU1 bigcap_setU1. Qed.

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

Proof.

by move=> Xx; rewrite (bigcup_setD1 x)// set_fsetD1. Qed.

Arguments bigcup_fsetD1 {T U} x.

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

Proof.

by move=> Xx; rewrite (bigcap_setD1 x)// set_fsetD1. Qed.

Arguments bigcup_fsetD1 {T U} x.

Section bigcup_seq.
Variables ( : choiceType) ( : Type).

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

Proof.

elim: s => [/=|h s ih]; first by rewrite set_nil bigcup_set0 big_nil.
rewrite big_cons -ih predeqE => u; split=> [[t /andP[]]|].
- rewrite inE => /orP[/eqP ->{t} -> fhu|ts Pt ftu]; first by left.
  case: ifPn => Ph; first by right; exists t => //; apply/andP; split.
  by exists t => //; apply/andP; split.
- case: ifPn => [Ph [fhu|[t /andP[ts Pt] ftu]]|Ph [t /andP[ts Pt ftu]]].
  + by exists h => //; apply/andP; split => //; rewrite mem_head.
  + by exists t => //; apply/andP; split => //; rewrite inE orbC ts.
  + by exists t => //; apply/andP; split => //; rewrite inE orbC ts.
Qed.

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

Proof.

rewrite -(bigcup_seq_cond s f xpredT); congr (\bigcup_( in mkset _) _).
by rewrite funeqE => t; rewrite andbT.
Qed.

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

Proof.

by apply: setC_inj; rewrite setC_bigcap setC_bigsetI bigcup_seq_cond. Qed.

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

Proof.

by apply: setC_inj; rewrite setC_bigcap setC_bigsetI bigcup_seq. Qed.

End bigcup_seq.

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

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

Proof.

rewrite -(big_mkord xpredT F) -bigcup_seq.
by apply: eq_bigcupl; split=> i; rewrite /= mem_index_iota leq0n.
Qed.

Lemma :
\bigcup_ \big[setU/set0]_( < k.+1) F i =
\bigcup_ \big[setU/set0]_( < k) F i.

Proof.

transitivity (\bigcup_( in S @` setT) \big[setU/set0]_( < k) F i).
by rewrite bigcup_image.
rewrite [RHS](bigcup_setD1 0%N)// big_ord0 set0U; apply: eq_bigcupl.
split=> [x [? _ <-//]|x [_ x0]]/=; exists x.-1 => //; rewrite prednK// lt0n.
exact/eqP.
Qed.

Lemma :
\bigcup_ \big[setU/set0]_( < k.+1) F i = \bigcup_ F k.

Proof.

apply/seteqP; split=> [x [i _]|x [i _ Fix]].
by rewrite -bigcup_mkord => -[j _ Fjx]; exists j.
by exists i => //; rewrite big_ord_recr/=; right.
Qed.

Lemma ( : 'I_n.+1 -> set T) :
\bigcup_( < n.+1) G (inord i) = \big[setU/set0]_( < n.+1) G i.

Proof.

rewrite bigcup_mkord; apply: eq_bigr => /= i _; congr G.
by apply/val_inj => /=; rewrite inordK.
Qed.

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

Proof.

by apply: setC_inj; rewrite setC_bigsetI setC_bigcap bigcup_mkord. Qed.

Lemma : (i < n)%N -> F i `<=` \big[setU/set0]_( < n) F j.

Proof.

by move: n => // n ni; rewrite -bigcup_mkord; exact/bigcup_sup. Qed.

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

Proof.

by rewrite -bigcup_mkord => x [k _ Fkx]; exists k. Qed.

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

Proof.

by rewrite -bigcup_mkord bigcup2inE. Qed.

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

Proof.

by rewrite -bigcap_mkord bigcap2inE. Qed.

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

Proof.

rewrite -bigcup_mkord -(bigcup_image _ (addn n)) -bigcup_setU.
apply: eq_bigcupl; split=> // k _.
have [ltkn|lenk] := ltnP k n; [left => //|right].
by exists (k - n); rewrite // subnKC.
Qed.

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

Proof.

by apply: setC_inj; rewrite setCI !setC_bigcap (bigcup_splitn n) setC_bigsetI.
Qed.

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

Proof.

move=> m n mn; rewrite -!bigcup_mkord => x [i im Fix].
by exists i => //=; rewrite (leq_trans im).
Qed.

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

Proof.

move=> m n mn; rewrite -setCS !setC_bigsetI.
exact: (@subset_bigsetU (setC \o F)).
Qed.

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

Proof.

move=> n m nm; rewrite big_mkcond [in X in _ `<=` X]big_mkcond/=.
exact: (@subset_bigsetU (fun => if P i then F i else _)).
Qed.

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

Proof.

move=> n m nm; rewrite big_mkcond [in X in _ `<=` X]big_mkcond/=.
exact: (@subset_bigsetI (fun => if P i then F i else _)).
Qed.

Lemma : \bigcup_ F (n + i) = \bigcup_( >= n) F i.

Proof.

rewrite eqEsubset; split => [x /= [m _ Fmnx]|x /= [m nm Fmx]].
- by exists (n + m) => //=; rewrite leq_addr.
- by exists (m - n) => //; rewrite subnKC.
Qed.

Lemma : \bigcap_ F (n + i) = \bigcap_( >= n) F i.

Proof.

rewrite eqEsubset; split=> [x /= Fnx m nm|x /= nFx m _].
- by rewrite -(subnKC nm); exact: Fnx.
- exact/nFx/leq_addr.
Qed.

End bigop_nat_lemmas.

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

Proof.

apply/predeqP => u; split=> [[x Px fxu]|]; first by rewrite (bigD1 x)//; left.
move=> /mem_set; rewrite (@big_morph _ _ (fun => u \in X) false orb).
- by move=> /= x y; apply/idP/orP; rewrite !inE.
- by rewrite in_set0.
- by rewrite big_has_cond => /hasP[x _ /andP[xP]]; rewrite inE => ufx; exists x.
Qed.

Section smallest.
Context {} ( : set T -> Prop).

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

Lemma : C X -> G `<=` X -> smallest G `<=` X.

Proof.

by move=> XC GX A; apply. Qed.

Lemma : smallest G `<=` X -> G `<=` X.

Proof.

by apply: subset_trans => t Gt B [CB]; exact. Qed.

Lemma : X `<=` G -> X `<=` smallest G.

Proof.

by move=> XG A /XG GA Y /= [PY]; exact. Qed.

Lemma : G `<=` smallest G

Proof.

exact: sub_smallest. Qed.

Lemma : C G -> smallest G = G.

Proof.

by move=> Cs; apply/seteqP; split; [exact: smallest_sub|exact: sub_smallest].
Qed.

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

Lemma {} ( : set T -> Prop) ( : set T) :
C Y -> smallest C X `<=` Y <-> X `<=` Y.

Proof.

by move=> CY; split; [exact: smallest_sub_sub|exact: smallest_sub].
Qed.

Definition {} ( : set T -> Prop) :=
forall ( : set_system T), MM `<=` C -> C (\bigcap_( in MM) A).

Section bigcap_closed_smallest.
Context {} ( : set T -> Prop).

Lemma ( : set T) : bigcap_closed C -> C (smallest C G).

Proof.

by apply; exact: subIsetl. Qed.

End bigcap_closed_smallest.

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

Proof.

by move=> CCG2 G12; apply: smallest_sub => //; exact: sub_smallest.
Qed.

Lemma {} ( : set T -> Prop) :
(forall , C2 G -> C1 G) ->
forall , smallest C1 G `<=` smallest C2 G.

Proof.

by move=> C12 G X sX M [/C12 C1M GM]; exact: sX. Qed.

Definition {} ( : set T) := forall , A x -> A y -> x = y.
Definition { } ( : T1 -> T2 -> Prop) := Logic.all (is_subset1 \o f).
Definition { } ( : T1 -> T2 -> Prop) := Logic.all (nonempty \o f).
Definition { } ( : T1 -> T2 -> Prop) :=
  forall , (f x !=set0) /\ is_subset1 (f x).

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

CoInductive { : choiceType} ( : set T) : T -> Prop -> Type :=
| of x = xget x0 P & P x : xget_spec x0 P x True
| of (forall , ~ P x) : xget_spec x0 P x0 False.

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

Proof.

move: (erefl (xget x0 P)); set y := {2}(xget x0 P).
rewrite /xget; case: pselect => /= [?|neqP _].
by case: sigW => x /= /asboolP Px; rewrite [P x]propT //; constructor.
suff NP x : ~ P x by rewrite [P x0]propF //; constructor.
by apply: contra_not neqP => Px; exists x; apply/asboolP.
Qed.

Lemma { : choiceType} ( : set T) : (exists , P x) -> P (xget x0 P).

Proof.

by case: xgetP=> // NP [x /NP]. Qed.

Lemma { : choiceType} ( : set T) ( : T): P x -> P (xget x0 P).

Proof.

by move=> Px; apply: xgetPex; exists x. Qed.

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

Proof.

by move=> Px /(_ _ _ (xgetI x0 Px) Px). Qed.

Lemma { : choiceType} ( : set T) ( : T) :
P x -> (forall , P y -> y = x) -> xget x0 P = x.

Proof.

by move=> /xget_subset1 gPx eqx; apply: gPx=> y z /eqx-> /eqx. Qed.

Lemma { : choiceType} ( : set T) :
(forall , ~ P x) -> xget x0 P = x0.

Proof.

by case: xgetP => // x _ Px /(_ x). Qed.

Definition {} { : choiceType} ( : aT -> rT)
( : aT -> rT -> Prop) := fun => xget (f0 x) (f x).

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

Proof.

by move=> [b fab]; rewrite /fun_of_rel; apply: xgetI fab. Qed.

Lemma {} { : choiceType}
( : aT -> rT -> Prop) ( : aT -> rT) :
is_subset1 (f a) -> forall , f a b -> fun_of_rel f0 f a = b.

Proof.

by move=> fa1 b /xget_subset1 xgeteq; rewrite /fun_of_rel xgeteq. Qed.

Lemma ( : set T) ( : { | x \in A} -> Prop) :
(forall : { | x \in A}, P u) =
(forall : T, forall ( : A u), P (exist _ u (mem_set a))).

Proof.

rewrite propeqE; split=> [+ u a|PA [u a]]; first exact.
have Au : A u by rewrite inE in a.
by rewrite (Prop_irrelevance a (mem_set Au)); apply: PA.
Qed.

Lemma {} ( : set U) ( : U -> Prop) :
{in A, forall , P x} <-> forall , A x -> P x.

Proof.

by split=> AP x; have := AP x; rewrite inE. Qed.

Lemma { } ( : set U) ( : set V) ( : U -> V -> Prop) :
{in A & B, forall , P x y} <-> (forall , A x -> B y -> P x y).

Proof.

by split=> AP x y; have := AP x y; rewrite !inE. Qed.

Lemma [] [ : T1 -> Prop] :
{in [set: T1], forall : T1, P1 x : Prop} -> forall : T1, P1 x : Prop.

Proof.

by move=> + *; apply; rewrite !inE. Qed.

Lemma [ ] [ : T1 -> T2 -> Prop] :
{in [set: T1] & [set: T2], forall ( : T1) ( : T2), P2 x y : Prop} ->
forall ( : T1) ( : T2), P2 x y : Prop.

Proof.

by move=> + *; apply; rewrite !inE. Qed.

Lemma [ ] [ : T1 -> T2 -> T3 -> Prop] :
{in [set: T1] & [set: T2] & [set: T3], forall ( : T1) ( : T2) ( : T3), P3 x y z : Prop} ->
forall ( : T1) ( : T2) ( : T3), P3 x y z : Prop.

Proof.

by move=> + *; apply; rewrite !inE. Qed.

Lemma [ : Type] [ : T1 -> T2] :
{in [set: T1], bijective f} -> bijective f.

Proof.

by case=> [g /in1TT + /in1TT +]; exists g. Qed.

. }.

()
. of isPointed T & Choice T}.

. () ( -> pointedType) :=
  isPointed.Build (forall : T, T' t) (fun=> point).

..Build unit tt.
..Build bool false.
..Build Prop False.
..Build nat 0.
. () :=
  isPointed.Build (T * T')%type (point, point).
. () (T : pointedType) :=
  isPointed.Build (n.-tuple T) (nseq n point).
. () :=
  isPointed.Build 'M[T]_(m, n) (\matrix_(_, _) point)%R.
. () := isPointed.Build (option T) None.
. () := isPointed.Build {fset T} fset0.

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

Section PointedTheory.
Context { : pointedType}.

Lemma ( : set T) : (exists , P x) -> P (get P).

Proof.

exact: (xgetPex point). Qed.

Lemma ( : set T) ( : T): P x -> P (get P).

Proof.

exact: (xgetI point). Qed.

Lemma ( : set T) ( : T) : P x -> is_subset1 P -> get P = x.

Proof.

exact: (xget_subset1 point). Qed.

Lemma ( : set T) ( : T) :
P x -> (forall , P y -> y = x) -> get P = x.

Proof.

exact: (xget_unique point). Qed.

Lemma ( : set T) : (forall , ~ P x) -> get P = point.

Proof.

exact: (xgetPN point). Qed.

Lemma : setT != set0 :> set T.

Proof.

by apply/eqP => /seteqP[] /(_ point) /(_ Logic.I). Qed.

End PointedTheory.

. () X := {
  zero : X;
  one : X;
  zero_one_neq : zero != one;
}.

()
.
  { of Choice X & isBiPointed X }.

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

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

Proof.

by move=> []. Qed.

.
-> False
}.

()
. of isEmpty T & Finite T}.

. T := {
axiom : T -> False
}.
. T.

Definition : T -> nat := fun=> 0%N.
Definition : nat -> option T := fun=> None.
Lemma : pcancel pickle unpickle.

Proof.

by move=> x; case: (axiom x). Qed.

..Build T pickleK.

Lemma : Finite.axiom ([::] : seq T).

Proof.

by move=> /[dup]/axiom. Qed.

..Build T fin_axiom.

..Build T axiom.
..

.
-> False
}.
. T.
Definition ( : T) := true.
Lemma : Equality.axiom eq_op

Proof.

by move=> ? /[dup]/axiom. Qed.

..Build T eq_opP.

Definition & pred T & nat : option T := None.
Lemma ( : pred T) ( : nat) ( : T) : find P n = Some x -> P x.

Proof.

by []. Qed.

Lemma ( : pred T) : (exists : T, P x) -> exists : nat, find P n.

Proof.

by move=> [/[dup]/axiom]. Qed.

Lemma ( : pred T) : P =1 Q -> find P =1 find Q.

Proof.

by []. Qed.

..Build T findP ex_find eq_find.

..Build T axiom.
..

..Build False id.

..Build void (@of_void _).

Definition { : emptyType} : T -> False := @axiom T.
Definition { : emptyType} {} : T -> U := @False_rect _ \o no.

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

Proof.

by move=> X; apply/setF_eq0/no. Qed.

Definition ( : C -> T) (  : emptyType -> T):=
    forall ( : T -> Type), (forall : emptyType, G (alt s)) -> (forall , G (sort x)) ->
  forall , G x.
Notation sort alt := (@quasi_canonical_of _ _ sort alt).
Notation T C := (@quasi_canonical_of T C id id).

Lemma ( : C -> T) ( : emptyType -> T) :
    (forall , (exists : emptyType, alt y = x) + (exists , sort y = x)) ->
  quasi_canonical_ sort alt.

Proof.

by move=> + G Cx Gs x => /(_ x)[/cid[y <-]|/cid[y <-]]. Qed.

Arguments qcanon {T C sort alt} x.

Lemma : quasi_canonical choiceType pointedType.

Proof.

apply: qcanon => -[Ts [Tc Te]].
set T := Choice.Pack _.
have [/unsquash x|/(_ (squash _)) TF] := pselect $|T|.
  right.
  pose Tp := isPointed.Build T x.
  pose TT : pointedType := HB.pack T Te Tc Tp.
  by exists TT.
left.
pose TMixin := Choice_isEmpty.Build T TF.
pose TT : emptyType := HB.pack T Te Tc TMixin.
by exists TT.
Qed.

Lemma : quasi_canonical eqType pointedType.

Proof.

by apply: qcanon; elim/eqPchoice; elim/choicePpointed => [[T F]|T];
[left; exists (Empty.Pack F) | right; exists T].
Qed.

Lemma : quasi_canonical Type pointedType.

Proof.

by apply: qcanon; elim/Peq; elim/eqPpointed => [[T F]|T];
[left; exists (Empty.Pack F) | right; exists T].
Qed.

Section partitions.

Definition ( : set I) ( : I -> set T) :=
forall : I, D i -> D j -> F i `&` F j !=set0 -> i = j.

Lemma ( : I) ( : I -> set T) : trivIset [set i] F.

Proof.

by move=> j k <- <-. Qed.

Lemma ( : nat -> set T) :
(forall , (m < n)%N -> F m `&` F n = set0) -> trivIset setT F.

Proof.

move=> h m n _ _ [t [mt nt]]; apply/eqP/negPn/negP.
by rewrite neq_ltn => /orP[] /h; apply/eqP/set0P; exists t.
Qed.

Lemma ( : nat -> set T) :
(forall , F n.+1 `<=` ~` (\big[setU/set0]_( < n.+1) F i)) -> trivIset setT F.

Proof.

move=> sF; apply: ltn_trivIset => n m h; rewrite setIC; apply/disjoints_subset.
by case: n h => // n h; apply: (subset_trans (sF n)); exact/subsetC/bigsetU_sup.
Qed.

Lemma ( : set I) ( : I -> set T) :
trivIset D F <-> trivIset setT (fun => if i \in D then F i else set0).

Proof.

split=> [tA i j _ _|tA i j Di Dj]; last first.
by have := tA i j Logic.I Logic.I; rewrite !mem_set.
case: ifPn => iD; last by rewrite set0I => -[].
by case: ifPn => [jD /tA|jD]; [apply; exact: set_mem|rewrite setI0 => -[]].
Qed.

Lemma { } ( : set I) : trivIset D (fun=> set0 : set T).

Proof.

by move=> i j Di Dj; rewrite setI0 => /set0P; rewrite eqxx. Qed.

Lemma {} { : eqType} { : set I} { : I -> set T} :
trivIset D F <->
forall : I, D i -> D j -> i != j -> F i `&` F j = set0.

Proof.

split=> tDF i j Di Dj; first by apply: contraNeq => /set0P/tDF->.
by move=> /set0P; apply: contraNeq => /tDF->.
Qed.

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

Proof.

move=> /trivIsetP tA; elim => [|n IHn] m Dm.
by move=> _; rewrite big_ord0 set0I.
move=> lt_nm; rewrite big_mkcond/= big_ord_recr -big_mkcond/=.
rewrite setIUl IHn 1?ltnW// set0U.
by case: ifPn => [Dn|NDn]; rewrite ?set0I// tA// ltn_eqF.
Qed.

Lemma ( : Type) ( : set I) ( : I -> set T) ( : I -> set T) :
trivIset D F -> trivIset D (fun => G i `&` F i).

Proof.

by move=> tF i j Di Dj [x [[Gix Fix] [Gjx Fjx]]]; apply tF => //; exists x.
Qed.

Lemma ( : Type) ( : set I) ( : I -> set T) ( : I -> set T) :
trivIset D F -> trivIset D (fun => F i `&` G i).

Proof.

by move=> tF i j Di Dj [x [[Fix Gix] [Fjx Gjx]]]; apply tF => //; exists x.
Qed.

Lemma ( : set I) ( : I -> set T) :
D `<=` D' -> trivIset D' F -> trivIset D F.

Proof.

by move=> DD' Ftriv i j /DD' + /DD' + /Ftriv->//. Qed.

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

Proof.

Lemma ( : set I) ( : I -> I') ( : I' -> set T) :
trivIset D (F \o f) -> trivIset (f @` D) F.

Proof.

by move=> trivF i j [{}i Di <-] [{}j Dj <-] Ffij; congr (f _); apply: trivF.
Qed.

Arguments trivIset_image {T I I'} D f F.

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

Proof.

move=> finj; apply/propext; split; first exact: trivIset_image.
move=> trivF i j Di Dj Ffij; apply: finj; rewrite ?in_setE//.
by apply: trivF => //=; [exists i| exists j].
Qed.

Lemma { } ( : aT -> rT) :
trivIset D (fun => f @^-1` [set x]).

Proof.

by move=> y z _ _ [x [<- <-]]. Qed.

Lemma {} { : choiceType} ( : set rT) ( : set aT)
( : aT -> rT) : trivIset D (fun => A `&` f @^-1` [set x]).

Proof.

by move=> y z _ _ [x [[_ <-] [_ <-]]]. Qed.

Lemma ( : Type) ( : eqType) ( : J -> set I) ( : I -> set T) :
  (forall , trivIset (D n) F) ->
  (forall , n != m -> D n i -> D m j -> F i `&` F j !=set0 -> i = j) ->
  trivIset (\bigcup_ D k) F.

Proof.

move=> tB H; move=> i j [n _ Dni] [m _ Dmi] ij.
have [nm|nm] := eqVneq n m; first by apply: (tB m) => //; rewrite -nm.
exact: (H _ _ _ _ nm).
Qed.

Lemma ( : eqType) ( : I -> set T1) ( : T1 -> set T2) :
  trivIset setT D ->
  trivIset (\bigcup_ D i) F ->
  trivIset setT (fun => \bigcup_( in D i) F t).

Proof.

move=> D0 h i j _ _ [t [[m Dim Fmt] [n Djn Fnt]]].
have mn : m = n by apply: h => //; [exists i|exists j|exists t].
rewrite {}mn {m} in Dim Fmt *.
by apply: D0 => //; exists n.
Qed.

Definition ( : I -> set T) := \bigcup_( in D) F i.

Lemma ( : I -> set T) : cover D F = \bigcup_( in D) F i.

Proof.

by []. Qed.

Lemma ( : I -> set T) :
D `<=` D' -> (forall , D' i -> ~ D i -> F i = set0) ->
cover D F = cover D' F.

Proof.

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

Proof.

move=> FG.
rewrite eqEsubset; split => [t [i Di Fit]|t [i Di Git]].
have [j Dj GF] : [set G i | in D] (F i) by rewrite -FG /mkset; exists i.
by exists j => //; rewrite GF.
have [j Dj GF] : [set F i | in D] (G i) by rewrite FG /mkset; exists i.
by exists j => //; rewrite GF.
Qed.

Definition ( : I -> set T) ( : set T) :=
  [/\ cover D F = A, trivIset D F & forall , D i -> F i !=set0].

Definition ( : pointedType) ( : I -> set T) ( : T) :=
  [get | D i /\ F i x].

Definition ( : pointedType) ( : I -> set T) ( : T) :=
  F (pblock_index D F x).

Notation X := (trivIset X id).

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

Proof.

exact: trivIset_image. Qed.

Lemma ( : I -> set T) :
D `<=` D' -> (forall , D' i -> ~ D i -> F i = set0) ->
trivIset D F = trivIset D' F.

Proof.

move=> DD' DD'F.
rewrite propeqE; split=> [DF i j D'i D'j FiFj0|D'F i j Di Dj FiFj0].
  have [Di|Di] := pselect (D i); last first.
    by move: FiFj0; rewrite (DD'F i) // set0I => /set0P; rewrite eqxx.
  have [Dj|Dj] := pselect (D j).
  - exact: DF.
  - by move: FiFj0; rewrite (DD'F j) // setI0 => /set0P; rewrite eqxx.
by apply D'F => //; apply DD'.
Qed.

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

Proof.

move=> s1D; rewrite perm_sym => /(perm_iotaP set0)[s ss1 s12] /trivIsetP ts1.
apply/trivIsetP => i j Di Dj ij.
rewrite {}s12 {s2}; have [si|si] := ltnP i (size s); last first.
  by rewrite (nth_default set0) ?size_map// set0I.
rewrite (nth_map O) //; have [sj|sj] := ltnP j (size s); last first.
  by rewrite setIC (nth_default set0) ?size_map// set0I.
have nth_mem k : k < size s -> nth O s k \in iota 0 (size s1).
  by move=> ?; rewrite -(perm_mem ss1) mem_nth.
rewrite (nth_map O)// ts1 ?(nth_uniq,(perm_uniq ss1),iota_uniq)//; apply/s1D.
- by have := nth_mem _ si; rewrite mem_iota leq0n add0n.
- by have := nth_mem _ sj; rewrite mem_iota leq0n add0n.
Qed.

End partitions.
#[deprecated(note="Use trivIset_setIl instead")]
Notation := trivIset_setIl (only parsing).

Section Zorn.

Definition ( : set T) ( : T -> T -> Prop) :=
  forall , A s -> A t -> R s t \/ R t s.

Let ( : Type) ( : rel T) ( : {pred T}) :
  (forall , total_on A R -> exists , forall , A s -> R s t) ->
  wo_chain R P -> exists2 , z \in predT & upper_bound R P z.

Proof.

move: R P; elim/Peq : T => T R P Atot RP.
suff : total_on P R by move=> /Atot[t ARt]; exists t.
move=> s t Ps Pt; have [| |] := RP [predU (pred1 s) & (pred1 t)].
- by move=> x; rewrite !inE => /orP[/eqP ->{x}|/eqP ->{x}].
- by exists s; rewrite !inE eqxx.
- move=> x [[]]; rewrite !inE => /orP[/eqP ->{x}|/eqP ->{x}].
+ by move=> /(_ t); rewrite !inE eqxx orbT => /(_ isT) Rst _; left.
+ by move=> /(_ s); rewrite !inE eqxx => /(_ isT) Rts _; right.
Qed.

Lemma ( : Type) ( : rel T) :
  (forall , R t t) -> (forall , R r s -> R s t -> R r t) ->
  (forall , R s t -> R t s -> s = t) ->
  (forall : set T, total_on A R -> exists , forall , A s -> R s t) ->
  exists , forall , R t s -> s = t.

Proof.

move: R; elim/Peq : T => T R Rxx Rtrans Ranti Atot.
have [//| |P _ RP|] := @Zorn's_lemma _ R predT _.
- by move=> ? ? ? _ _ _; exact: Rtrans.
- exact: total_on_wo_chain.
by move=> x _ Rx; exists x => s Rxs; apply: (Ranti _ _ _ Rxs) => //; exact: Rx.
Qed.

Definition ( : T -> T -> Prop) ( : T) :=
  forall , R t s -> R s t.

Lemma ( : Type) ( : T) ( : rel T) :
  (forall , R t t) -> (forall , R r s -> R s t -> R r t) ->
  (forall , total_on A R -> exists , forall , A s -> R s t) ->
  exists , premaximal R t.

Proof.

move: t0 R; elim/Peq : T => T t0 R Rxx Rtrans Atot.
have [//| | |z _ Hz] := @Zorn's_lemma T R predT.
- by move=> ? ? ? _ _ _; exact: Rtrans.
- by move=> A _ RA; exact: total_on_wo_chain.
by exists z => s Rzs; exact: Hz.
Qed.

End Zorn.

Section Zorn_subset.
Variables ( : Type) ( : set_system T).

Lemma :
    (forall : set_system T, F `<=` P -> total_on F subset ->
      P (\bigcup_( in F) X)) ->
  exists , P A /\ forall , A `<` B -> ~ P B.

Proof.

move=> totP; pose R ( : P) := `[< sval sA `<=` sval sB >].
have {}totR F ( : total_on F R) : exists , forall , F sA -> R sA sB.
   have FP : [set val x | in F] `<=` P.
     by move=> _ [X FX <-]; apply: set_mem; exact/valP.
   have totF : total_on [set val x | in F] subset.
     move=> _ _ [X FX <-] [Y FY <-].
     by have [/asboolP|/asboolP] := FR _ _ FX FY; [left|right].
   exists (SigSub (mem_set (totP _ FP totF))) => A FA.
   exact/asboolP/(bigcup_sup (imageP val _)).
have [| | |sA sAmax] := Zorn _ _ _ totR.
- by move=> ?; apply/asboolP; exact: subset_refl.
- by move=> ? ? ? /asboolP ? /asboolP st; apply/asboolP; exact: subset_trans st.
- by move=> [A PA] [B PB] /asboolP AB /asboolP BA; exact/eq_exist/seteqP.
- exists (val sA); case: sA => A PA /= in sAmax *; split; first exact: set_mem.
  move=> B AB PB.
  have : R (exist (fun : T -> Prop => x \in P) A PA) (SigSub (mem_set PB)).
    by apply/asboolP; exact: properW.
  move=> /(sAmax (SigSub (mem_set PB)))[BA].
  by move: AB; rewrite BA; exact: properxx.
Qed.

End Zorn_subset.

Definition ( : I -> set T) ( : set I) :=
  [/\ A `<=` B, trivIset A F & forall ,
      A `<` C -> C `<=` B -> ~ trivIset C F ].

Section maximal_disjoint_subcollection.
Context { : Type}.
Variables ( : I -> set T) ( : set I).

Let := fun => X `<=` D /\ trivIset X B.

Let ( : set_system I) :
  A `<=` P -> total_on A (fun => x `<=` y) -> P (\bigcup_( in A) x).

Proof.

move=> AP h; split; first by apply: bigcup_sub => E /AP [].
move=> i j [x Ax] xi [y Ay] yj ij; have [xy|yx] := h _ _ Ax Ay.
- by apply: (AP _ Ay).2 => //; exact: xy.
- by apply: (AP _ Ax).2 => //; exact: yx.
Qed.

Lemma :
{ | maximal_disjoint_subcollection B E D }.

Proof.

have /cid[E [[ED tEB] maxE]] := Zorn_bigcup maxP.
by exists E; split => // F /maxE + FD; exact: contra_not.
Qed.

End maximal_disjoint_subcollection.

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

Definition : set T := [set | forall , A x -> (x <= y)%O].
Definition : set T := [set | forall , A x -> (y <= x)%O].

Lemma : (forall , A y -> (y <= x)%O) <-> ubound A x.

Proof.

by []. Qed.

Lemma : (forall , A y -> (x <= y)%O) <-> lbound A x.

Proof.

by []. Qed.

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

Proof.

by rewrite propeqE; split => [/(_ x erefl)//|xy z ->]. Qed.

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

Proof.

by rewrite propeqE; split => [/(_ x erefl)//|xy z ->]. Qed.

Lemma : lbound (ubound [set x]) y -> (y <= x)%O.

Proof.

by move/(_ x); apply; rewrite ub_set1. Qed.

Lemma : ubound (lbound [set x]) y -> (x <= y)%O.

Proof.

by move/(_ x); apply; rewrite lb_set1. Qed.

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

Proof.

by move=> y; apply. Qed.

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

Proof.

by move=> y; apply. Qed.

Lemma : ubound A y -> lbound (ubound A) x -> (x <= y)%O.

Proof.

by move=> Ay; apply. Qed.

Lemma : lbound A y -> ubound (lbound A) x -> (y <= x)%O.

Proof.

by move=> Ey; apply. Qed.

Definition : set T := [set | exists , A y /\ (x <= y)%O].

Definition := ubound A !=set0.
Definition := (A !=set0) /\ has_ubound A.
Definition := lbound A !=set0.
Definition := (A !=set0) /\ has_lbound A.

Lemma : has_ubound [set x].

Proof.

by exists x; rewrite ub_set1. Qed.

Lemma : ~ has_inf (@set0 T).

Proof.

by rewrite /has_inf not_andP; left; exact/nonemptyPn. Qed.

Lemma : ~ has_sup (@set0 T).

Proof.

by rewrite /has_sup not_andP; left; exact/nonemptyPn. Qed.

Lemma : has_sup [set x].

Proof.

by split; [exists x | exists x => y ->]. Qed.

Lemma : has_inf [set x].

Proof.

by split; [exists x | exists x => y ->]. Qed.

Lemma : A `<=` B -> has_lbound B -> has_lbound A.

Proof.

by move=> AB [l Bl]; exists l => a Aa; exact/Bl/AB. Qed.

Lemma : A `<=` B -> has_ubound B -> has_ubound A.

Proof.

by move=> AB [l Bl]; exists l => a Aa; exact/Bl/AB. Qed.

Lemma : (exists2 , A y & (x <= y)%O) <-> down A x.

Proof.

by split => [[y Ay xy]|[y [Ay xy]]]; [exists y| exists y]. Qed.

Definition := ubound A m /\ forall , ubound A b -> (m <= b)%O.

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

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

Proof.

rewrite /supremums predeqE => y; split => [[]|->{y}]; last first.
by split; [rewrite ub_set1|exact: lb_ub_refl].
by rewrite ub_set1 => xy /lb_ub_set1 yx; apply/eqP; rewrite eq_le xy yx.
Qed.

Lemma : is_subset1 (supremums A).

Proof.

move=> x y [Ax xA] [Ay yA]; apply/eqP.
by rewrite eq_le (ub_lb_ub Ax yA) (ub_lb_ub Ay xA).
Qed.

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

Lemma : ~ has_sup A -> supremum x0 A = x0.

Proof.

move=> hsA; rewrite /supremum; case: ifPn => // /set0P[/= x Ax].
case: xgetP => //= _ -> [uA _]; exfalso.
by apply: hsA; split; [exists x|exists (xget x0 (supremums A))].
Qed.

Lemma : supremum x0 set0 = x0.

Proof.

by rewrite /supremum eqxx. Qed.

Lemma : supremum x0 [set x] = x.

Proof.

rewrite /supremum ifF.
by apply/eqP; rewrite predeqE => /(_ x)[+ _]; apply.
by rewrite supremums1; case: xgetP => // /(_ x) /(_ erefl).
Qed.

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

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

Proof.

rewrite /infimums predeqE => y; split => [[]|->{y}]; last first.
by split; [rewrite lb_set1|apply ub_lb_refl].
by rewrite lb_set1 => xy /ub_lb_set1 yx; apply/eqP; rewrite eq_le xy yx.
Qed.

Lemma : is_subset1 (infimums A).

Proof.

move=> x y [Ax xA] [Ay yA]; apply/eqP.
by rewrite eq_le (lb_ub_lb Ax yA) (lb_ub_lb Ay xA).
Qed.

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

End UpperLowerTheory.

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

Lemma :
supremums A !=set0 -> A t -> (supremum x0 A >= t)%O.

Proof.

case=> x Ax; rewrite /supremum; case: ifPn => [/eqP -> //|_].
by case: xgetP => [y yA [uAy _]|/(_ x) //]; exact: uAy.
Qed.

Lemma :
infimums A !=set0 -> A t -> (infimum x0 A <= t)%O.

Proof.

case=> x Ex; rewrite /infimum; case: ifPn => [/eqP -> //|_].
by case: xgetP => [y yE [uEy _]|/(_ x) //]; exact: uEy.
Qed.

End UpperLowerOrderTheory.

Lemma ( : set nat) : ubound A !=set0 -> supremums A !=set0.

Proof.

case => /=; elim => [A0|n ih]; first by exists O.
case: (pselect (ubound A n)) => [/ih //|An {ih}] An1.
exists n.+1; split => // m Am; case/existsNP : An => k /not_implyP[Ak /negP].
rewrite -Order.TotalTheory.ltNge => kn.
by rewrite (Order.POrderTheory.le_trans _ (Am _ Ak)).
Qed.

Definition ( : set_system T) :=
forall , F A -> G B -> A `&` B !=set0.

Notation := (meets F G) : classical_set_scope.

Section meets.

Lemma ( : set_system T) : F `#` G = G `#` F.

Proof.

gen have sFG : F G / F `#` G -> G `#` F.
by move=> FG B A => /FG; rewrite setIC; apply.
by rewrite propeqE; split; apply: sFG.
Qed.

Lemma ( : set_system T) :
F `<=` F' -> G `<=` G' -> F' `#` G' -> F `#` G.

Proof.

by move=> sF sG FG A B /sF FA /sG GB; apply: (FG A B). Qed.

Lemma ( : set_system T) : G `<=` G' -> F `#` G' -> F `#` G.

Proof.

exact: sub_meets. Qed.

Lemma ( : set_system T) : F `<=` F' -> F' `#` G -> F `#` G.

Proof.

by move=> /sub_meets; apply. Qed.

End meets.

Fact : Order.disp_t

Proof.

by []. Qed.

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

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

Proof.

by apply/asboolP/eqP; rewrite setIidPl. Qed.

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

Proof.

apply/idP/idP => [/asboolP|/andP[BA /asboolP AB]]; rewrite properEneq eq_sym;
by [move=> [] -> /asboolP|apply/asboolP].
Qed.

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

Proof.

by rewrite setUC setKU. Qed.

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

Proof.

by rewrite setIC setKI. Qed.

. (set T) := Choice.copy _ (set T).

.
  Order.isMeetJoinDistrLattice.Build set_display (set T)
    le_def lt_def (@setIC _) (@setUC _) (@setIA _) (@setUA _)
    joinKI meetKU (@setIUl _) setIid.

Lemma : (set0 <= A)%O.

Proof.

by apply/asboolP; exact: sub0set. Qed.

Lemma : (A <= setT)%O.

Proof.

exact/asboolP. Qed.

..hasBottom.Build set_display (set T)
SetOrder_sub0set.

..hasTop.Build set_display (set T)
SetOrder_setTsub.

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

Proof.

by rewrite setDE setICA setICr setI0. Qed.

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

Proof.

by rewrite setUC -setDDr setDv setD0. Qed.

..BDistrLattice_hasSectionalComplement.Build
set_display (set T) subKI joinIB.

..CBDistrLattice_hasComplement.Build
set_display (set T) (fun => esym (setTD x)).

End SetOrder.
Module . HB.reexport. End Exports.
End Internal.

Module .

Export Internal.Exports.

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

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

Proof.

by rewrite asboolE. Qed.

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

Proof.

by rewrite asboolE. Qed.

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

Proof.

by []. Qed.

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

Proof.

by []. Qed.

Lemma : \bot%O = @set0 T

Proof.

by []. Qed.

Lemma : \top%O = @setT T

Proof.

by []. Qed.

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

Proof.

by []. Qed.

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

Proof.

by []. Qed.

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

Proof.

by apply: (iffP idP); rewrite subsetEset. Qed.

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

Proof.

by apply: (iffP idP); rewrite properEset. Qed.

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

Section seqD.
Variable : Type.
Implicit Types F : (set T)^nat.

Definition := F n `\` \big[setU/set0]_( < n) F k.

Lemma : trivIset setT (seqDU F).

Proof.

move=> i j _ _; wlog ij : i j / (i < j)%N => [/(_ _ _ _) tB|].
by have [ij /tB->|ij|] := ltngtP i j; rewrite //setIC => /tB ->.
move=> /set0P; apply: contraNeq => _; apply/eqP.
rewrite /seqDU 2!setDE !setIA setIC (bigD1 (Ordinal ij)) //=.
by rewrite setCU setIAC !setIA setICl !set0I.
Qed.

Definition := fun => if n isn't n'.+1 then F O else F n `\` F n'.

Lemma : nondecreasing_seq F -> seqDU F = seqD F.

Proof.

move=> ndF; rewrite funeqE => -[|n] /=; first by rewrite /seqDU big_ord0 setD0.
rewrite /seqDU big_ord_recr /= setUC; congr (_ `\` _); apply/setUidPl.
by rewrite -bigcup_mkord => + [k /= kn]; exact/subsetPset/ndF/ltnW.
Qed.

Lemma : nondecreasing_seq F -> trivIset setT (seqD F).

Proof.

by move=> ndF; rewrite -seqDU_seqD //; exact: trivIset_seqDU. Qed.

Lemma : \bigcup_ seqD F n = \bigcup_ F n.

Proof.

Lemma : \bigcup_ F k = \bigcup_ seqDU F k.

Proof.

rewrite /seqDU predeqE => t; split=> [[n _ Fnt]|[n _]]; last first.
by rewrite setDE => -[? _]; exists n.
have [UFnt|UFnt] := pselect ((\big[setU/set0]_( < n) F k) t); last by exists n.
suff [m [Fmt FNmt]] : exists , F m t /\ forall , (k < m)%N -> ~ F k t.
by exists m => //; split => //; rewrite -bigcup_mkord => -[k kj]; exact: FNmt.
move: UFnt; rewrite -bigcup_mkord => -[/= k _ Fkt] {Fnt n}.
have [n kn] := ubnP k; elim: n => // n ih in t k Fkt kn *.
case: k => [|k] in Fkt kn *; first by exists O.
have [?|] := pselect (forall , (m <= k)%N -> ~ F m t); first by exists k.+1.
move=> /existsNP[i] /not_implyP[ik] /contrapT Fit; apply: (ih t i) => //.
by rewrite (leq_ltn_trans ik).
Qed.

End seqD.
Arguments trivIset_seqDU {T} F.
#[global] Hint Resolve trivIset_seqDU : core.

Section product.
Variables ( : Type).
Implicit Type A B : set (T1 * T2).

Lemma : {homo @fst_set T1 T2 : / A `<=` B}.

Proof.

by move=> A B AB x [y Axy]; exists y; exact/AB. Qed.

Lemma : {homo @snd_set T1 T2 : / A `<=` B}.

Proof.

by move=> A B AB x [y Axy]; exists y; exact/AB. Qed.

Lemma : A `<=` A.`1 \o fst

Proof.

by move=> [x y]; exists y. Qed.

Lemma : A `<=` A.`2 \o snd

Proof.

by move=> [x y]; exists x. Qed.

Lemma ( : set T1) ( : set T2) : (X `*` Y).`1 `<=` X.

Proof.

by move=> x [y [//]]. Qed.

Lemma ( : set T1) ( : set T2) : (X `*` Y).`2 `<=` Y.

Proof.

by move=> x [y [//]]. Qed.

Lemma ( : set T1) ( : T1 -> set T2) : (X `*`` Y).`1 `<=` X.

Proof.

by move=> x [y [//]]. Qed.

End product.

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

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

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

Lemma : xsection A x `<=` A.`2.

Proof.

by move=> y Axy; exists x; rewrite /xsection/= inE in Axy. Qed.

Lemma : ysection A y `<=` A.`1.

Proof.

by move=> x Axy; exists y; rewrite /ysection/= inE in Axy. Qed.

Lemma : (y \in xsection A x) = ((x, y) \in A).

Proof.

by apply/idP/idP => [|]; [rewrite inE|rewrite /xsection !inE /= inE]. Qed.

Lemma : xsection A x y <-> A (x, y).

Proof.

by rewrite /xsection/= inE. Qed.

Lemma : (x \in ysection A y) = ((x, y) \in A).

Proof.

by apply/idP/idP => [|]; [rewrite inE|rewrite /ysection !inE /= inE]. Qed.

Lemma : ysection A y x <-> A (x, y).

Proof.

by rewrite /ysection/= inE. Qed.

Lemma : xsection A x = (fun => (x, y)) @^-1` A.

Proof.

by apply/seteqP; split => [y|y] /xsectionP. Qed.

Lemma : ysection A y = (fun => (x, y)) @^-1` A.

Proof.

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

Lemma : xsection set0 x = set0.

Proof.

by rewrite xsectionE preimage_set0. Qed.

Lemma : ysection set0 y = set0.

Proof.

by rewrite ysectionE preimage_set0. Qed.

Lemma : x \in X1 -> xsection (X1 `*` X2) x = X2.

Proof.

move=> xX1; apply/seteqP; split=> [y /xsection_snd_set|]; first exact: snd_setX.
by move=> y X2y; rewrite /xsection/= inE; split=> //=; rewrite inE in xX1.
Qed.

Lemma : y \in X2 -> ysection (X1 `*` X2) y = X1.

Proof.

move=> yX2; apply/seteqP; split=> [x /ysection_fst_set|]; first exact: fst_setX.
by move=> x X1x; rewrite /ysection/= inE; split=> //=; rewrite inE in yX2.
Qed.

Lemma : x \notin X1 -> xsection (X1 `*` X2) x = set0.

Proof.

move=> xX1; rewrite /xsection /= predeqE => y; split => //.
by rewrite /xsection/= inE => -[] /=; rewrite notin_setE in xX1.
Qed.

Lemma : y \notin X2 -> ysection (X1 `*` X2) y = set0.

Proof.

move=> yX2; rewrite /xsection /= predeqE => x; split => //.
by rewrite /ysection/= inE => -[_]; rewrite notin_setE in yX2.
Qed.

Lemma ( : nat -> set (T1 * T2)) :
xsection (\bigcup_ F n) x = \bigcup_ xsection (F n) x.

Proof.

rewrite predeqE /xsection => y; split => [|[n _]] /=; rewrite inE.
by move=> -[n _ Fnxy]; exists n => //=; rewrite inE.
by move=> Fnxy; rewrite inE; exists n.
Qed.

Lemma ( : nat -> set (T1 * T2)) :
ysection (\bigcup_ F n) y = \bigcup_ ysection (F n) y.

Proof.

rewrite predeqE /ysection => x; split => [|[n _]] /=; rewrite inE.
by move=> -[n _ Fnxy]; exists n => //=; rewrite inE.
by move=> Fnxy; rewrite inE; exists n.
Qed.

Lemma ( : nat -> set (T1 * T2)) : trivIset setT F ->
trivIset setT (fun => xsection (F n) x).

Proof.

move=> /trivIsetP h; apply/trivIsetP => i j _ _ ij.
rewrite /xsection /= predeqE => y; split => //= -[]; rewrite !inE => Fixy Fjxy.
by have := h i j Logic.I Logic.I ij; rewrite predeqE => /(_ (x, y))[+ _]; apply.
Qed.

Lemma ( : nat -> set (T1 * T2)) : trivIset setT F ->
trivIset setT (fun => ysection (F n) y).

Proof.

move=> /trivIsetP h; apply/trivIsetP => i j _ _ ij.
rewrite /ysection /= predeqE => x; split => //= -[]; rewrite !inE => Fixy Fjxy.
by have := h i j Logic.I Logic.I ij; rewrite predeqE => /(_ (x, y))[+ _]; apply.
Qed.

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

Proof.

by move=> X Y XY y; rewrite /xsection /= 2!inE => /XY. Qed.

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

Proof.

by move=> X Y XY x; rewrite /ysection /= 2!inE => /XY. Qed.

Lemma : xsection (A `&` B) x = xsection A x `&` xsection B x.

Proof.

by rewrite /xsection predeqE => y/=; split; rewrite !inE => -[]. Qed.

Lemma : ysection (A `&` B) y = ysection A y `&` ysection B y.

Proof.

by rewrite /ysection predeqE => x/=; split; rewrite !inE => -[]. Qed.

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

Proof.

by rewrite predeqE /xsection /= => y; split; rewrite !inE. Qed.

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

Proof.

by rewrite predeqE /ysection /= => x; split; rewrite !inE. Qed.

Lemma ( : set T2) : xsection (snd @^-1` B) x = B.

Proof.

by apply/seteqP; split; move=> y/=; rewrite /xsection/= inE. Qed.

Lemma ( : set T1) : ysection (fst @^-1` A) y = A.

Proof.

by apply/seteqP; split; move=> x/=; rewrite /ysection/= inE. Qed.

End section.

Notation :=
([set | exists2 , A (xy.1, z) & B (z, xy.2)]) : relation_scope.

Notation := ([set | A (xy.2, xy.1)]) : relation_scope.

Section relation.
Local Open Scope relation_scope.

Lemma { : Type} ( : set (X * Y)) ( : set (Y * X)) :
A `<=` C -> B `<=` D -> A \; B `<=` C \; D.

Proof.

by move=> AsubC BD [x z] /= [y] Bxy Ayz; exists y; [exact: BD | exact: AsubC].
Qed.

Lemma { : Type} ( : set (T * T)) :
E \; range (fun => (x, x)) = E.

Proof.

rewrite eqEsubset; split => [[_ _] [_ [_ _ [<- <-//]]]|[x y] Exy]/=.
by exists x => //; exists x.
Qed.

Lemma { : Type} ( : set (T * T)) : E^-1^-1 = E.

Proof.

by rewrite eqEsubset; split; case. Qed.

Definition { : Type} := [set : T * T | x.1 = x.2].

Lemma { : Type} ( : T) : diagonal (x, y) <-> x = y.

Proof.

by []. Qed.

End relation.

Section powerset.
Context { : Type}.
Implicit Types (a b : T) (A B : set T).

Lemma : [set | X `<=` set0] = [set set0] :> set_system T.

Proof.

by apply/funext => X /=; rewrite subset0. Qed.

Lemma : [set | X `<=` [set a]] = [set set0; [set a]].

Proof.

by apply/seteqP; split => X/=; [move/subset_set1|case=> ->]. Qed.

Lemma :
[set | X `<=` [set a; b]] = [set set0; [set a]; [set b]; [set a; b]].

Proof.

apply/seteqP; split => X/=; first by move/subset_set2; rewrite or4E !orA.
by move=> [[[]|]|] ->.
Qed.

Lemma : (A `<=` B) = ([set | X `<=` A] `<=` [set | X `<=` B]).

Proof.

apply: propext; split; first by move=> AB X/= /subset_trans; apply.
by move=> + a Aa => /(_ [set a])/= /(_ _ a); apply => // ? ->.
Qed.

Lemma :
A `<=` B -> `[A, B] = setU A @` [set | X `<=` B `\` A].

Proof.

move=> AB; apply/seteqP; split => Y/=.
rewrite in_itv/= => /andP[]; rewrite !subsetEset => AY YB.
by exists (Y `\` A); [exact: setSD | rewrite setDUK].
case=> X XBA <-; rewrite in_itv/= Order.JoinTheory.leUl/=.
by rewrite -(setDUK AB) Order.JoinTheory.leU2// subsetEset.
Qed.

Lemma :
A `<=` B -> `[A, B] = setU^~ A @` [set | X `<=` B `\` A].

Proof.

by (under eq_imagel do rewrite setUC); exact: setorder_itv_setUl_image.
Qed.

Lemma :
A `<=` B -> `[A, B] = setD B @` [set | X `<=` B `\` A].

Proof.

move=> AB; apply/seteqP; split => Y/=.
  rewrite in_itv/= => /andP[]; rewrite !subsetEset => AY YB.
  by exists (B `\` Y); [exact: setDS | rewrite setDD setIidr].
case=> X XBA <-; rewrite in_itv/= Order.MeetTheory.leIl andbT.
rewrite (@Order.POrderTheory.le_trans _ _ (B `\` (B `\` A)))//.
  by rewrite setDD setIidr.
by rewrite subsetEset; exact: setDS.
Qed.

End powerset.

Files

Module mathcomp.classical.classical_sets