Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)

Notation "[ predI _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ predU _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ predD _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ predC _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ preim _ of _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
New coercion path [GRing.subring_closedM;
                   GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing 
[GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.subring_closed_semi;
                   GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing 
[GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed.
New coercion path [GRing.subring_closed_semi;
                   GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing 
[GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.sdivr_closed_div;
                   GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing 
[GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.subalg_closedBM;
                   GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing 
[GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.divring_closed_div;
                   GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing 
[GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.divalg_closedBdiv;
                   GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing 
[GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.Pred.subring_smul;
                   GRing.Pred.smul_mul] : GRing.Pred.subring >-> GRing.Pred.mul is ambiguous with existing 
[GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.subring >-> GRing.Pred.mul.
[ambiguous-paths,typechecker]

From mathcomp Require Import ssrint interval.

Notation "_ \* _" was already used in scope
ring_scope. [notation-overridden,parsing]
Notation "\- _" was already used in scope ring_scope.
[notation-overridden,parsing]


(******************************************************************************)
(* This file develops a basic theory of sets and types equipped with a        *)
(* canonical inhabitant (pointed types).                                      *)
(*                                                                            *)
(* --> A decidable equality is defined for any type. It is thus possible to   *)
(*     define an eqType structure for any type using the mixin gen_eqMixin.   *)
(* --> This file adds the possibility to define a choiceType structure for    *)
(*     any type thanks to an axiom gen_choiceMixin giving a choice mixin.     *)
(* --> We chose to have generic mixins and no global instances of the eqType  *)
(*     and choiceType structures to let the user choose which definition of   *)
(*     equality to use and to avoid conflict with already declared instances. *)
(*                                                                            *)
(* * Sets:                                                                    *)
(*                       set T == type of sets on T.                          *)
(*                   (x \in P) == boolean membership predicate from ssrbool   *)
(*                                for set P, available thanks to a canonical  *)
(*                                predType T structure on sets on T.          *)
(*             [set x : T | P] == set of points x : T such that P holds.      *)
(*                 [set x | P] == same as before with T left implicit.        *)
(*            [set E | x in A] == set defined by the expression E for x in    *)
(*                                set A.                                      *)
(*   [set E | x in A & y in B] == same as before for E depending on 2         *)
(*                                variables x and y in sets A and B.          *)
(*                        setT == full set.                                   *)
(*                        set0 == empty set.                                  *)
(*                     range f == the range of f, i.e. [set f x | x in setT]  *)
(*                     [set a] == set containing only a.                      *)
(*                 [set a : T] == same as before with the type of a made      *)
(*                                explicit.                                   *)
(*                     A `|` B == union of A and B.                           *)
(*                      a |` A == A extended with a.                          *)
(*        [set a1; a2; ..; an] == set containing only the n elements ai.      *)
(*                     A `&` B == intersection of A and B.                    *)
(*                     A `*` B == product of A and B, i.e. set of pairs (a,b) *)
(*                                such that A a and B b.                      *)
(*                        A.`1 == set of points a such that there exists b so *)
(*                                that A (a, b).                              *)
(*                        A.`2 == set of points a such that there exists b so *)
(*                                that A (b, a).                              *)
(*                        ~` A == complement of A.                            *)
(*                    [set~ a] == complement of [set a].                      *)
(*                     A `\` B == complement of B in A.                       *)
(*                      A `\ a == A deprived of a.                            *)
(*                        `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 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 F == same as before with T left implicit.        *)
(*                smallest C G := \bigcap_(A in [set M | C M /\ G `<=` M]) A  *)
(*                   A `<=` B <-> A is included in B.                         *)
(*                  A `<=>` B <-> double inclusion A `<=` B and B `<=` A.     *)
(*                   f @^-1` A == preimage of A by f.                         *)
(*                      f @` A == image of A by f. Notation for `image A f`.  *)
(*                    A !=set0 := exists x, A x.                              *)
(*                    [set` p] == a classical set corresponding to the        *)
(*                                predType p                                  *)
(*                     `[a, b] := [set` `[a, b]], i.e., a classical set       *)
(*                                corresponding to the interval `[a, b].      *)
(*                     `]a, b] := [set` `]a, b]]                              *)
(*                     `[a, b[ := [set` `[a, b[]                              *)
(*                     `]a, b[ := [set` `]a, b[]                              *)
(*                   `]-oo, b] := [set` `]-oo, b]]                            *)
(*                   `]-oo, b[ := [set` `]-oo, b[]                            *)
(*                   `[a, +oo[ := [set` `[a, +oo[]                            *)
(*                   `]a, +oo[ := [set` `]a, +oo[]                            *)
(*                 `]-oo, +oo[ := [set` `]-oo, +oo[]                          *)
(*               is_subset1 A <-> A contains only 1 element.                  *)
(*                   is_fun f <-> for each a, f a contains only 1 element.    *)
(*                 is_total f <-> for each a, f a is non empty.               *)
(*              is_totalfun f <-> conjunction of is_fun and is_total.         *)
(*                   xget x0 P == point x in P if it exists, x0 otherwise;    *)
(*                                P must be a set on a choiceType.            *)
(*             fun_of_rel f0 f == function that maps x to an element of f x   *)
(*                                if there is one, to f0 x otherwise.         *)
(*                    F `#` G <-> intersections beween elements of F an G are *)
(*                                all non empty.                              *)
(*                                                                            *)
(* * Pointed types:                                                           *)
(*                 pointedType == interface type for types equipped with a    *)
(*                                canonical inhabitant.                       *)
(*             PointedType T m == packs the term m : T to build a             *)
(*                                pointedType; T must have a choiceType       *)
(*                                structure.                                  *)
(*   [pointedType of T for cT] == T-clone of the pointedType structure cT.    *)
(*          [pointedType of T] == clone of a canonical pointedType structure  *)
(*                                on T.                                       *)
(*                       point == canonical inhabitant of a pointedType.      *)
(*                       get P == point x in P if it exists, point otherwise; *)
(*                                P must be a set on a pointedType.           *)
(*                                                                            *)
(* --> Thanks to this basic set theory, we proved Zorn's Lemma, which states  *)
(*     that any ordered set such that every totally ordered subset admits an  *)
(*     upper bound has a maximal element. We also proved an analogous version *)
(*     for preorders, where maximal is replaced with premaximal: t is         *)
(*     premaximal if whenever t < s we also have s < t.                       *)
(*                                                                            *)
(*                      $| T | == T : Type is inhabited                       *)
(*                    squash x == proof of $| T | (with x : T)                *)
(*                  unsquash s == extract a witness from s : $| T |           *)
(* --> Tactic:                                                                *)
(*   - squash x:                                                              *)
(*     solves a goal $| T | by instantiating with x or [the T of x]           *)
(*                                                                            *)
(*                trivIset D F == the sets F i, where i ranges over D : set I,*)
(*                                are pairwise-disjoint                       *)
(*                   cover D F := \bigcup_(i in D) F i                        *)
(*             partition D F A == the non-empty sets F i,where i ranges over  *)
(*                                D : set I, form a partition of A            *)
(*          pblock_index D F x == index i such that i \in D and x \in F i     *)
(*                pblock D F x := F (pblock_index D F x)                      *)
(*                                                                            *)
(* * Upper and lower bounds:                                                  *)
(*              ubound A == the set of upper bounds of the set A              *)
(*              lbound A == the set of lower bounds of the set A              *)
(*   Predicates to express existence conditions of supremum and infimum of    *)
(*   sets of real numbers:                                                    *)
(*          has_ubound A := ubound A != set0                                  *)
(*             has_sup A := A != set0 /\ has_ubound A                         *)
(*          has_lbound A := lbound A != set0                                  *)
(*             has_inf A := A != set0 /\ has_lbound A                         *)
(*                                                                            *)
(*             isLub A m := m is a least upper bound of the set A             *)
(*           supremums A := set of supremums of the set A                     *)
(*         supremum x0 A == supremum of A or x0 if A is empty                 *)
(*            infimums A := set of infimums of the set A                      *)
(*          infimum x0 A == infimum of A or x0 if A is empty                  *)
(*                                                                            *)
(*               F `#` G := the classes of sets F and G intersect             *)
(*                                                                            *)
(* * sections:                                                                *)
(*           xsection A x == with A : set (T1 * T2) and x : T1 is the         *)
(*                           x-section of A                                   *)
(*           ysection A y == with A : set (T1 * T2) and y : T2 is the         *)
(*                           y-section of A                                   *)
(*                                                                            *)
(* * About the naming conventions in this file:                               *)
(* - use T, T', T1, T2, etc., aT (domain type), rT (return type) for names of *)
(*   variables in Type (or choiceType/pointedType/porderType)                 *)
(*   + use the same suffix or prefix for the sets as their containing type    *)
(*     (e.g., A1 in T1, etc.)                                                 *)
(*   + as a consequence functions are rather of type aT -> rT                 *)
(* - use I, J when the type corresponds to an index                           *)
(* - sets are named A, B, C, D, etc., or Y when it is ostensibly an image set *)
(*   (i.e., of type set rT)                                                   *)
(* - indexed sets are rather named F                                          *)
(*                                                                            *)
(* * Composition of relations:                                                *)
(*                A \; B == [set x | exists z, A (x.1, z) & B (z, x.2)]       *)
(*                                                                            *)
(******************************************************************************)

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

Declare Scope classical_set_scope.


The only parsing modifier has no effect in Reserved
Notation.
[irrelevant-reserved-notation-only-parsing,parsing]

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

Notation "\bigcup_ ( _ : _ ) _" was already defined
with a different format.
[notation-incompatible-format,parsing]

Reserved Notation "\bigcup_ ( i < n ) F"
  (at level 41, F at level 41, i, n at level 50,
           format "'[' \bigcup_ ( i  <  n ) '/  '  F ']'").
Reserved Notation "\bigcup_ i F"
  (at level 41, F at level 41, i at level 0,
           format "'[' \bigcup_ i '/  '  F ']'").
Reserved Notation "\bigcap_ ( i 'in' P ) F"
  (at level 41, F at level 41, i, P at level 50,
           format "'[' \bigcap_ ( i  'in'  P ) '/  '  F ']'").

Notation "\bigcap_ ( _ : _ ) _" was already defined
with a different format.
[notation-incompatible-format,parsing]

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

Definition set T := T -> Prop.
(* we use fun x => instead of pred to prevent inE from working *)
(* we will then extend inE with in_setE to make this work      *)
Definition in_set T (A : set T) : pred T := (fun x => `[<A x>]).
Canonical set_predType T := @PredType T (set T) (@in_set T).


T: Type
A: set T
x: T
(x \in A) = A x


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

Definition inE := (inE, in_setE).

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

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

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

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

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

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

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

Definition setT := [set _ : T | True].
Definition set0 := [set _ : T | False].
Definition set1 (t : T) := [set x : T | x = t].
Definition setI A B := [set x | A x /\ B x].
Definition setU A B := [set x | A x \/ B x].
Definition nonempty A := exists a, A a.
Definition setC A := [set a | ~ A a].
Definition setD A B := [set x | A x /\ ~ B x].
Definition setM T1 T2 (A1 : set T1) (A2 : set T2) := [set z | A1 z.1 /\ A2 z.2].
Definition fst_set T1 T2 (A : set (T1 * T2)) := [set x | exists y, A (x, y)].
Definition snd_set T1 T2 (A : set (T1 * T2)) := [set y | exists x, A (x, y)].
Definition setMR T1 T2 (A1 : set T1) (A2 : T1 -> set T2) :=
  [set z | A1 z.1 /\ A2 z.1 z.2].
Definition setML T1 T2 (A1 : T2 -> set T1) (A2 : set T2) :=
  [set z | A1 z.2 z.1 /\ A2 z.2].


T, rT: Type
P: T -> Prop
b
[set x | P x] x = P x


f
 by []. Qed.

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

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

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

Definition proper A B := A `<=` B /\ ~ (B `<=` A).

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

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

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

Notation "\bigcup_ ( i 'in' P ) F" :=
  (bigcup P (fun i => F)) : classical_set_scope.
Notation "\bigcup_ ( i : T ) F" :=
  (\bigcup_(i in @setT T) F) : classical_set_scope.
Notation "\bigcup_ ( i < n ) F" :=
  (\bigcup_(i in `I_n) F) : classical_set_scope.
Notation "\bigcup_ i F" := (\bigcup_(i : _) F) : classical_set_scope.
Notation "\bigcap_ ( i 'in' P ) F" :=
  (bigcap P (fun i => F)) : classical_set_scope.
Notation "\bigcap_ ( i : T ) F" :=
  (\bigcap_(i in @setT T) F) : classical_set_scope.
Notation "\bigcap_ ( i < n ) F" :=
  (\bigcap_(i in `I_n) F) : classical_set_scope.
Notation "\bigcap_ i F" := (\bigcap_(i : _) F) : classical_set_scope.

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

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

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

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


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


17
 by rewrite inE. Qed.


9
1a
1b
1c
y: rT
f @^-1` `]y, +oo[ = [set x | (y < f x)%O]


21

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


23
f @^-1` `[y, +oo[ = [set x | (y <= f x)%O]


28

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


9
1a
rT: orderType d
1c
24
f @^-1` `]-oo, y[ = [set x | (f x < y)%O]


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


2f
f @^-1` `]-oo, y] = [set x | (f x <= y)%O]


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


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


39
 by move=> /funext->. Qed.

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

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


P, T: Type
set0 -> P
 
40
 by case=> x; rewrite inE. Qed.


9
D: {pred T}
pred_oapp D = mem [set Some x | x in fun x : T => D x]


47


9
4a
b
x \in D ->
ex2 (fun x : T => D x)
  (fun x0 : T => Some x0 = Some x)
50
ex2 (fun x : T => D x)
  (fun x0 : T => Some x0 = Some x) -> x \in D
49
(exists2 x : T, D x & Some x = None) -> false


4e
 
50
54
55


59
 
49
56


5e
 by case.
Qed.


9
D: set T
pred_oapp (mem D) = mem [set Some x | x in D]


62

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 {T : Type}.
Implicit Types A B C D : set T.


9
a
u: T
A u -> u \in A
 
69
 by rewrite inE. Qed.

6b
u \in A -> A u
 
70
 by rewrite inE. Qed.

9
6c
u \in [set: T]
 
75
 by rewrite inE. Qed.

6b
cancel mem_set set_mem
 
7b
 by []. Qed.

6b
cancel set_mem mem_set
 
80
 by []. Qed.


6b
~ A u -> (u \in A) = false


85
 by apply: contra_notF; rewrite inE. Qed.


8
(x \notin A : Prop) = (~ A x)


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


9
a
A != [set: T] <-> (exists t : T, ~ A t)


8f


91
~ A == [set: T] -> exists t : T, ~ A t


9
a
h: forall x : T, ~ ~ A x
A == [set: T]

by apply/eqP; rewrite predeqE => t; split => // _; apply: contrapT.
Qed.
#[deprecated(note="Use setTPn instead")]
Notation setTP := setTPn.


9
b
(x \in set0) = false
 
9f
 by rewrite memNset. Qed.

a1
x \in [set: T]
 
a5
 by rewrite mem_set. Qed.


9
b
a
(x \in ~` A) = (x \notin A)


aa
 by apply/idP/idP; rewrite inE notin_set. Qed.


9
b
A, B: set T
(x \in A `&` B) = (x \in A) && (x \in B)


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


b2
(x \in A `\` B) = (x \in A) && (x \notin B)


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


b2
(x \in A `|` B) = (x \in A) || (x \in B)


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


T, T': Type
x: (T * T')%type
a
E: set T'
(x \in A `*` E) = (x.1 \in A) && (x.2 \in E)


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


9
a
x: A
A (val x)


ca
 by apply: set_mem; apply: valP. Qed.


9
b3
(A = B) = (A `<=>` B)


d1


9
b3
AB: A `<=` B
BA: B `<=` A
A = B

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


d3
A = B <-> A `<=>` B
 
de
 by rewrite eqEsubset. Qed.


9
[set` predT] = [set: T]


e3
 by apply/seteqP; split. Qed.


e5
[set` pred0] = set0


e9
 by apply/seteqP; split. Qed.


9
P, Q: {pred T}
[set` predI P Q] = [set` P] `&` [set` Q]


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


f0
[set` predU P Q] = [set` P] `|` [set` Q]


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


e5
(fun=> true) = [set: T]


fa
 by rewrite [LHS]set_true. Qed.


e5
(fun=> false) = set0


ff
 by rewrite [LHS]set_false. Qed.


91
[set` A] = A


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


9
P: pred T
mem [set` P] = mem P


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


91
A `<=` A
 
110
 by []. Qed.


9
B, A, C: set T
A `<=` B -> B `<=` C -> A `<=` C


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


91
set0 `<=` A
 
11c
 by []. Qed.


e5
~` set0 = [set: T]


121
 by rewrite predeqE; split => ?. Qed.


e5
involutive setC


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


e5
~` [set: T] = set0
 
12b
 by rewrite -setC0 setCK. Qed.

Definition setC_inj := can_inj setCK.


e5
commutative setI


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


9
C, A, B: set T
A `<=` B -> C `&` A `<=` C `&` B


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


137
A `<=` B -> A `&` C `<=` B `&` C


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


9
A, B, C, D: set T
A `<=` C -> B `<=` D -> A `&` B `<=` C `&` D


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


e5
right_id [set: T] setI


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


e5
left_id [set: T] setI


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


e5
right_zero set0 setI


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


e5
left_zero set0 setI


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


e5
left_inverse set0 setC setI


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


e5
right_inverse set0 setC setI


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


e5
associative setI


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


e5
left_commutative setI


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


e5
right_commutative setI


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


e5
interchange setI setI


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


e5
idempotent setI


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


9
A, B, C: set T
A `&` B `&` C = A `&` C `&` (B `&` C)


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


181
A `&` (B `&` C) = A `&` B `&` (A `&` C)


186
 by rewrite !(setIC A) setIIl. Qed.


e5
commutative setU


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


137
A `<=` B -> C `|` A `<=` C `|` B


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


137
A `<=` B -> A `|` C `<=` B `|` C


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


143
A `<=` C -> B `<=` D -> A `|` B `<=` C `|` D


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


e5
left_zero [set: T] setU


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


e5
right_zero [set: T] setU


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


e5
left_id set0 setU


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


e5
right_id set0 setU


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


e5
left_inverse [set: T] setC setU


1b3


91
~` A `|` A = [set: T]

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


e5
right_inverse [set: T] setC setU


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


e5
associative setU


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


e5
left_commutative setU


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


e5
right_commutative setU


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


e5
interchange setU setU


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


e5
idempotent setU


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


181
A `|` B `|` C = A `|` C `|` (B `|` C)


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


181
A `|` (B `|` C) = A `|` B `|` (A `|` C)


1df
 by rewrite !(setUC A) setUUl. Qed.


d3
A `\` B = A `&` ~` B
 
1e4
 by []. Qed.


d3
A `<=` B -> A `|` B `\` A = B


1e9


9
b3
da
b
Bx: B x
(A `|` B `\` A) x

by have [Ax|nAx] := pselect (A x); [left|right].
Qed.


d3
A `<=` B -> B `\` A `|` A = B


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


91
A `\` A = set0


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


91
A `|` ~` A = [set: T]


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


1b8
 
1b8
 by rewrite setUC setUv. Qed.


d3
A `|` B `|` ~` B = [set: T]


205
 by rewrite -setUA setUv setUT. Qed.


d3
~` A `|` (A `|` B) = [set: T]


20a
 by rewrite setUA setvU setTU. Qed.


d3
A `&` B `&` ~` B = set0


20f
 by rewrite -setIA setICr setI0. Qed.


d3
~` A `&` (A `&` B) = set0


214
 by rewrite setIA setICl set0I. Qed.


d3
A `&` (B `\` A) = set0


219
 by rewrite setDE setICA -setDE setDv setI0. Qed.


d3
(B `\` A) `&` A = set0


21e
 by rewrite setIC setDIK. Qed.


9
a: T
a
A a -> a |` A `\ a = A


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


9
a
226
A `&` [set a] = (if a \in A then [set a] else set0)


22a

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


22c
[set a] `&` A = (if a \in A then [set a] else set0)


230
 by rewrite setIC setI1. Qed.


91
(A `<=` set0) = (A = set0)


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


91
([set: T] `<=` A) = (A = [set: T])


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


ac
([set x] `<=` A) = (x \in A)


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


91
A `<=` [set: T]
 
244
 by []. Qed.


d3
A = B -> A `<=` B
 
249
 by move->. Qed.

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


d3
[disjoint A & B] = (A `&` B == set0)


24e
 by []. Qed.


d3
reflect (A `&` B = set0) [disjoint A & B]%classic


253
 exact/eqP. Qed.


d3
reflect (A `&` B `<=` set0) [disjoint A & B]%classic


258
 by rewrite subset0; apply: disj_set2P. Qed.


d3
[disjoint B & A] = [disjoint A & B]


25d
 by rewrite !disj_set2E setIC. Qed.


d3
reflect (A `<=` B) [disjoint A & ~` B]%classic


262


9
b3
P: A `&` ~` B `<=` set0
t: T
_Hyp_: A t
B t

by apply: contrapT => ?; apply: (P t).
Qed.


d3
reflect (A `<=` B) [disjoint ~` B & A]%classic


26f
 by rewrite disj_set_sym; apply: disj_setPCl. Qed.


d3
reflect (A `<=` ~` B) [disjoint A & B]%classic


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


d3
reflect (B `<=` ~` A) [disjoint A & B]%classic


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


d3
A `<=` B <-> A `&` ~` B = set0


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


d3
A `&` B = set0 <-> A `<=` ~` B


283
 by rewrite subsets_disjoint setCK. Qed.


ac
(A `<=` [set~ x]) = (x \in ~` A)


288


ac
(~` A) x -> A `<=` [set~ x]

by move=> NAx y; apply: contraPnot => ->.
Qed.


137
A `<=` B -> A `\` C `<=` B `\` C


291
 by rewrite !setDE; apply: setSI. Qed.


91
[set: T] `\` A = ~` A


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


91
A != set0 <-> A !=set0


29b


9
a
A_neq0: ~ A == set0
A !=set0


9
a
2a3
A0: forall x : T, ~ A x
A = set0

by rewrite eqEsubset; split.
Qed.


e5
(T -> False) -> all_equal_to (set0 : set T)


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


d3
A `<=` B -> A !=set0 -> B !=set0


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


d3
A `<=` B -> ~` B `<=` ~` A


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


d3
~` A `<=` B -> ~` B `<=` A


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


d3
A `<=` ~` B -> B `<=` ~` A


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


d3
~` A `<=` ~` B -> B `<=` A


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


d3
~` A `<=` ~` B <-> B `<=` A


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


d3
~` A `<=` B <-> ~` B `<=` A


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


d3
A `<=` ~` B <-> B `<=` ~` A


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


d3
A `<=` A `|` B
 
2d9
 by move=> x; left. Qed.


d3
B `<=` A `|` B
 
2de
 by move=> x; right. Qed.


181
(B `|` C `<=` A) = (B `<=` A /\ C `<=` A)


2e3


181
B `|` C `<=` A -> B `<=` A /\ C `<=` A

by move=> sBC_A; split=> x ?; apply sBC_A; [left | right].
Qed.


d3
A `&` B = A <-> A `<=` B


2ec


9
b3
da
26b
(A `&` B) t <-> A t

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


d3
A `&` B = B <-> B `<=` A


2f6
 by rewrite setIC setIidPl. Qed.


d3
A `<=` B -> A `&` B = A
 
2fb
 by rewrite setIidPl. Qed.

d3
B `<=` A -> A `&` B = B
 
300
 by rewrite setIidPr. Qed.


d3
A `|` B = A <-> B `<=` A


305


9
b3
db
A `|` B = A

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


d3
A `|` B = B <-> A `<=` B


30f
 by rewrite setUC setUidPl. Qed.


d3
B `<=` A -> A `|` B = A
 
314
 by rewrite setUidPl. Qed.

d3
A `<=` B -> A `|` B = B
 
319
 by rewrite setUidPr. Qed.


181
(A `<=` B `&` C) = (A `<=` B /\ A `<=` C)


31e

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


d3
A `\` B = A <-> A `&` B = set0


323


9
b3
AB: forall x : T, (A `&` ~` B) x <-> A x
26b
A t -> (~` B) t
9
b3
AB: A `<=` ~` B
26b
(A `&` ~` B) t <-> A t


32f
331

by split=> [[]//|At]; move: (AB t At).
Qed.


d3
A `&` B = set0 -> A `\` B = A


336
 by move=> /setDidPl. Qed.


181
A `<=` C \/ B `<=` C -> A `&` B `<=` C


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


d3
A `&` B `<=` A
 
340
 by move=> x []. Qed.


d3
A `&` B `<=` B
 
345
 by move=> x []. Qed.


d3
A `\` B `<=` A


34a
 by rewrite setDE; apply: subIsetl. Qed.


d3
A `\` B `<=` ~` B


34f
 by rewrite setDE; apply: subIsetr. Qed.


143
A `<=` B ->
C `<=` D -> A `&` C !=set0 -> B `&` D !=set0


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


143
A `<=` B ->
C `<=` D -> B `&` D = set0 -> A `&` C = set0


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


d3
(A `\` B = set0) = (A `<=` B)


35e


9
b3
ADB0: A `\` B = set0
226
A a -> B a
9
b3
sAB: A `<=` B
A `\` B = set0

  
36a
36c

by rewrite predeqE => ?; split=> // - [?]; apply; apply: sAB.
Qed.


d3
(A `<` B) = (A != B /\ A `<=` B)


371


9
b3
BA: ~ B `<=` A
da
A != B /\ A `<=` B
d3
A <> B -> A `<=` B -> ~ B `<=` A /\ A `<=` B

  
d3
37d

by rewrite eqEsubset => AB BA; split => //; exact: contra_not AB.
Qed.


d3
~ A `<=` B -> A `&` ~` B !=set0


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


d3
(A `|` B = set0) = (A = set0 /\ B = set0)


387
 by rewrite -!subset0 subUset. Qed.


d3
(~` A `<=` ~` B) = (B `<=` A)


38c


2c6
30c
~` A `<=` ~` B

  
30c
394

by apply/subsets_disjoint; rewrite setCK setIC; apply/subsets_disjoint.
Qed.


91
A `\` [set: T] = set0


399
 by rewrite setDE setCT setI0. Qed.


91
set0 `\` A = set0


39e
 by rewrite setDE set0I. Qed.


91
A `\` set0 = A


3a3
 by rewrite setDE setC0 setIT. Qed.


137
A `<=` B -> C `\` B `<=` C `\` A


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


143
A `<=` C -> D `<=` B -> A `\` B `<=` C `\` D


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


d3
~` (A `|` B) = ~` A `&` ~` B


3b2


9
b3
z: T
(~` (A `|` B)) z <-> (~` A `&` ~` B) z

by apply: asbool_eq_equiv; rewrite asbool_and !asbool_neg asbool_or negb_or.
Qed.


d3
~` (A `&` B) = ~` A `|` ~` B


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


181
A `\` (B `|` C) = (A `\` B) `&` (A `\` C)


3c2
 by rewrite !setDE setCU setIIr. Qed.


e5
left_distributive setI setU


3c7


9
182
26b
((A `|` B) `&` C) t -> (A `&` C `|` B `&` C) t
3ce
(A `&` C `|` B `&` C) t -> ((A `|` B) `&` C) t

  
3ce
3d2

by move=> [[At Ct]|[Bt Ct]]; split => //; [left|right].
Qed.


e5
right_distributive setI setU


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


e5
left_distributive setU setI


3dc


3ce
(A `&` B `|` C) t -> ((A `|` C) `&` (B `|` C)) t
3ce
((A `|` C) `&` (B `|` C)) t -> (A `&` B `|` C) t

  
3ce
3e6

by move=> [[At|Ct] [Bt|Ct']]; by [left|right].
Qed.


e5
right_distributive setU setI


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


d3
(A `|` B) `&` A = A


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


d3
A `&` (B `|` A) = A


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


d3
A `&` B `|` A = A


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


d3
A `|` B `&` A = A


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


e5
left_distributive setD setU


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


d3
A `&` B `<=` set0 -> (A `|` B) `\` A = B


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


d3
A `&` B `<=` set0 -> (B `|` A) `\` A = B


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


181
A `&` (B `\` C) = A `&` B `\` C


413
 by rewrite !setDE setIA. Qed.


d3
A `\` (A `\` B) = A `&` B


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


181
A `\` B `\` C = A `\` (B `|` C)


41d
 by rewrite !setDE setCU setIA. Qed.


181
A `\` (B `\` C) = A `\` B `|` A `&` C


422
 by rewrite !setDE setCI setIUr setCK. Qed.


181
A `\` B `&` C = A `\` B `|` A `\` C


427
 by rewrite !setDE setCI setIUr. Qed.


d3
A `&` B `|` A `\` B = A


42c
 by rewrite setUC -setDDr setDv setD0. Qed.


c4
a
A `*` set0 = set0


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


c4
A: set T'
set0 `*` A = set0


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


c4
[set: T] `*` [set: T'] = [set: T * T']


43e
 exact/predeqP. Qed.


T, T1, T2: Type
A: set T1
A `*` [set: T2] = fst @^-1` A


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


447
B: set T2
[set: T1] `*` B = snd @^-1` B


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


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


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


447
C, D: set T1
A, B: set T2
A `<=` B -> C `<=` D -> C `*` A `<=` D `*` B


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


T, T1, T2, I: Type
F: I -> set T2
P: set I
448
A `*` \bigcup_(i in P) F i =
\bigcup_(i in P) (A `*` F i)


465


468
469
46a
448
x: T1
y: T2
(\bigcup_(i in P) (A `*` F i)) (x, y) ->
(A `*` \bigcup_(i in P) F i) (x, y)

by move=> [n Pn [/= Ax Fny]]; split => //; exists n.
Qed.


467
\bigcup_(i in P) F i `*` A =
\bigcup_(i in P) (F i `*` A)


475


468
469
46a
448
x: T2
y: T1
(\bigcup_(i in P) (F i `*` A)) (x, y) ->
(\bigcup_(i in P) F i `*` A) (x, y)

by move=> [n Pn [/= Ax Fny]]; split => //; exists n.
Qed.


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


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


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


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

End basic_lemmas.
#[global]
Hint Resolve subsetUl subsetUr subIsetl subIsetr subDsetl subDsetr : core.
#[deprecated(since="mathcomp-analysis 0.6", note="Use setICl instead.")]
Notation setvI := setICl.
#[deprecated(since="mathcomp-analysis 0.6", note="Use setICr instead.")]
Notation setIv := setICr.


TA, TB, rT: Type
A: set TA
B: set TB
f: TA -> TB -> rT
[set f x y | x in A & y in B] =
[set uncurry f x | x in A `*` B]


491

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


T: choiceType
[set` [::]] = set0


49b
 by rewrite predeqP. Qed.


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


4a2


4a5
h: T
t: seq T
[set` h :: t] h <-> set0 h -> h :: t = [::]

by rewrite /= mem_head => -[/(_ erefl)].
Qed.


49e
S: {fset T}
([set` S] == set0) = (S == fset0)


4b1
 by rewrite set_seq_eq0. Qed.

Section InitialSegment.


`I_0 = set0
 
4b8
 by rewrite predeqE. Qed.


`I_1 = [set 0]
 
4bd
 by rewrite predeqE; case. Qed.


n: nat
`I_n = set0 -> n = 0


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


4c4
`I_n.+1 = `I_n `|` [set n]


4c9


n, i: nat
i < n.+1 -> ((fun k : nat => k < n) `|` [set n]) i
4d0
i < n -> i < n.+1


4d0
4d5

by move/ltn_trans; apply.
Qed.


4c4
`I_n.+1 = n |` `I_n


4da
 by rewrite setUC IIS. Qed.


4c4
`I_n.+1 `\ n = `I_n


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


m, n: nat
`I_m `&` `I_n = `I_(minn m n)


4e4

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


4e6
`I_m `|` `I_n = `I_(maxn m n)


4eb

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


4c4
[set` iota 0 n] = `I_n


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

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


4c4
cancel ordII IIord


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


4c4
cancel IIord ordII


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

End InitialSegment.


[set: unit] = [set tt]


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


A: set unit
A = set0 \/ A = [set: unit]


504


507
Att: A tt
A = [set: unit]

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


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


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


B: set bool
[\/ B == [set true], B == [set false], B == set0
  | B == [set: bool]]


516


519
Bt: true \in B
Bf: false \in B
51a
519
520
Bf: false \notin B
51a
519
Bt: true \notin B
521
51a
519
528
525
51a


51d
 
51f
[\/ [set: bool] == [set true],
    [set: bool] == [set false], [set: bool] == set0
  | [set: bool] == [set: bool]]
522

  
524
51a
526529


531
 
524
B = [set true]
533

  
524
false \in B -> [set true] false
533

  
527
51a
529


53e
 
527
B = [set false]
540

  
527
true \in B -> [set false] true
540

  
52a
51a


54b
 
52a
B = set0

  by apply/seteqP; split => -[]//=; rewrite 2!notin_set in Bt, Bf.
Qed.

(* TODO: other lemmas that relate fset and classical sets *)

49e
A, B: {fset T}
[disjoint A & B]%fset = [disjoint [set` A] & [set` B]]


553


555
~~ [disjoint [set` A] & [set` B]]%classic ->
(A `&` B)%fset != fset0
555
(A `&` B)%fset != fset0 ->
~~ [disjoint [set` A] & [set` B]]%classic


555
55f

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

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


49d
[set` fset0] = set0


564
 by rewrite -subset0 => x. Qed.


49e
b
[set` [fset x]%fset] = [set x]


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


555
[set` (A `&` B)%fset] = [set` A] `&` [set` B]


56f

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


49e
P: {pred T}
A: {fset T}
[set` [fset x | x in A & P x]%fset] =
[set` A] `&` [set` P]


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


555
[set` (A `|` B)%fset] = [set` A] `|` [set` B]


57c


49e
556
b
(x \in A) || (x \in B) -> x \in A \/ x \in B
583
x \in A \/ x \in B -> (x \in A) || (x \in B)

  
583
587

by move=> []->; rewrite ?orbT.
Qed.


49e
b
578
[set` (x |` A)%fset] = x |` [set` A]


58c
 by rewrite set_fsetU set_fset1. Qed.


555
[set` (A `\` B)%fset] = [set` A] `\` [set` B]


592


583
(x \notin B) && (x \in A) -> x \in A /\ ~ x \in B

by case/andP => /negP xNB xA.
Qed.


49e
578
b
[set` (A `\ x)%fset] = [set` A] `\ x


59b
 by rewrite set_fsetD set_fset1. Qed.


49e
key: unit
K: choiceType
f: T -> K
p: finmempred T
[set` imfset key f p] = [set f x | x in [set` p]]


5a1


49e
5a4
5a5
5a6
5a7
x: K
[set f x | x in [set` p]] x -> [set` imfset key f p] x

by move=> [i ip <-]; apply: in_imfset.
Qed.

End SetFset.

Section SetMonoids.
Variable (T : Type).

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

End SetMonoids.

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


aT, rT: Type
f: aT -> rT
A: set aT
a: aT
A a -> [set f x | x in A] (f a)
 
5b1
 by exists a. Qed.


5b4
5b5
5b7
range f (f a)


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


5b3
injective f -> [set f x | x in A] (f a) = A a


5c1

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


5b4
5b6
[set x | x in A] = A


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


5b4
5b6
Y: set rT
5b5
{homo f : x / x \in A >-> x \in Y} <->
{homo f : x / A x >-> Y x}


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


5ce
[set f x | x in A] `<=` Y <->
{homo f : x / A x >-> Y x}


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


5b4
5b5
5b6
B: set rT
([set f x | x in A] `<=` B) = (A `<=` f @^-1` B)


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


5b4
5b5
A, B: set aT
[set f x | x in A `|` B] =
[set f x | x in A] `|` [set f x | x in B]


5df


5b4
5b5
5e2
b: rT
[set f x | x in A `|` B] b ->
([set f x | x in A] `|` [set f x | x in B]) b
5e8
([set f x | x in A] `|` [set f x | x in B]) b ->
[set f x | x in A `|` B] b


5e6
 
5e8
5ed


5f0
 by case=> -[] a Ha <-; apply imageP; [left | right].
Qed.


5b4
5b5
[set f x | x in set0] = set0


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


5b4
5b6
5b5
[set f x | x in A] = set0 -> A = set0


5fa


5b4
5b6
5b5
fA0: [set f x | x in A] = set0
t: aT
At: A t
set0 t

by have : set0 (f t) by rewrite -fA0; exists t.
Qed.


5b4
5b5
604
[set f x | x in [set t]] = [set f t]


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


5b4
5b6
5b7
A `<=` [set a] -> A = set0 \/ A = [set a]


60e


5b4
5b6
5b7
Aa: A `<=` [set a]
604
605
A = set0 \/ A = [set a]

by right; rewrite eqEsubset; split => // ? ->; rewrite -(Aa _ At).
Qed.


5b4
5b6
a, b: aT
A `<=` [set a; b] ->
[\/ A = set0, A = [set a], A = [set b]
  | A = [set a; b]]


61a


61c
A `<=` [set a; a] ->
[\/ A = set0, A = [set a], A = [set a]
  | A = [set a; a]]
5b4
5b6
61d
ab: a <> b
Aab: A `<=` [set a; b]
[\/ A = set0, A = [set a], A = [set b]
  | A = [set a; b]]

  
626
629


626
A `<=` [set a] ->
[\/ A = set0, A = [set a], A = [set b]
  | A = [set a; b]]
5b4
5b6
61d
627
628
x: aT
Ab: A b
629

  
633
629


633
A `<=` [set b] ->
[\/ A = set0, A = [set a], A = [set b]
  | A = [set a; b]]
5b4
5b6
61d
627
628
634
635
y: aT
Aa: A a
629

  
63f
629

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


5e1
[set f x | x in A `&` B]
`<=` [set f x | x in A] `&` [set f x | x in B]


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


5b4
5b5
5b6
[set f x | x in A] !=set0 -> A !=set0


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


5e1
A `<=` B -> [set f x | x in A] `<=` [set f x | x in B]


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


5f6
f @^-1` set0 = set0
 
656
 exact/predeqP. Qed.


5f6
f @^-1` [set: rT] = [set: aT]
 
65b
 by []. Qed.


5b4
5b5
5cf
f @^-1` Y !=set0 -> Y !=set0


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


64d
A `<=` f @^-1` [set f x | x in A]


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


aT, rT, A, B: Type
f: A -> B
f @^-1` range f = [set: A]


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


662
[set f x | x in f @^-1` Y] `<=` Y


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


662
range f = [set: rT] -> [set f x | x in f @^-1` Y] = Y


678


5b4
5b5
5cf
fsurj: range f = [set: rT]
x: rT
Y x -> [set f x | x in f @^-1` Y] x


5b4
5b5
5cf
680
681
Yx: Y x
[set: rT] x -> [set f x | x in f @^-1` Y] x

by rewrite -fsurj => - [y _ fy_eqx]; exists y => //=; rewrite fy_eqx.
Qed.


aT, rT, T1, T2: Type
448
f, f': T1 -> T2
(forall x : T1, A x -> f x = f' x) ->
[set f x | x in A] = [set f' x | x in A]


68a

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


5b4
g: aT -> aT
5b6
(forall x : aT, A x -> g x = x) ->
[set g x | x in A] = A


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


5b4
5b5
Y1, Y2: set rT
f @^-1` (Y1 `|` Y2) = f @^-1` Y1 `|` f @^-1` Y2


699
 exact/predeqP. Qed.


69b
f @^-1` (Y1 `&` Y2) = f @^-1` Y1 `&` f @^-1` Y2


6a0
 exact/predeqP. Qed.


662
~` f @^-1` Y = f @^-1` (~` Y)


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


69b
Y1 `<=` Y2 -> f @^-1` Y1 `<=` f @^-1` Y2


6aa
 by move=> Y12 t /Y12. Qed.


69b
f @^-1` (Y1 `&` Y2) !=set0 <->
f @^-1` Y1 `&` f @^-1` Y2 !=set0


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


aT, rT, I: Type
46a
5b5
F: I -> set rT
f @^-1` (\bigcup_(i in P) F i) =
\bigcup_(i in P) f @^-1` F i


6b4
 exact/predeqP. Qed.


6b6
f @^-1` (\bigcap_(i in P) F i) =
\bigcap_(i in P) f @^-1` F i


6bc
 exact/predeqP. Qed.


aT, rT, I, T: Type
D: set I
a
F, G: I -> T
{in D, F =1 G} -> D `&` F @^-1` A = D `&` G @^-1` A


6c1


6c4
6c5
a
6c6
eqFG: {in D, F =1 G}
i: I
(D `&` F @^-1` A) i <-> (D `&` G @^-1` A) i

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


aT, rT, T, R: Type
65
f: T -> R
i: R
i \notin [set f x | x in D] ->
D `&` f @^-1` [set i] = set0


6d1

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


aT, rT, T1, T2, T3: Type
A: set T3
g: T1 -> T2
f: T2 -> T3
(f \o g) @^-1` A = g @^-1` (f @^-1` A)


6da
 by []. Qed.


aT, rT, T: Type
a
id @^-1` A = A
 
6e4
 by []. Qed.


68d
g: T1 -> rT
f: T2 -> rT
C: set T1
f @^-1` [set g x | x in C] =
[set x | f x \in [set g x | x in C]]


6eb


68d
6ee
6ef
6f0
t: T2
(exists2 x : T1, C x & g x = f t) ->
f t \in [set g x | x in C]
6f6
f t \in [set g x | x in C] ->
exists2 x : T1, C x & g x = f t

  
6f6
6fb

by rewrite inE => -[r Cr <-]; exists r.
Qed.


69b
f @^-1` (Y1 `&` Y2) = set0 <->
f @^-1` Y1 `&` f @^-1` Y2 = set0


700

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


662
Y = set0 -> f @^-1` Y = set0


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


6d4
6d5
A: set R
A `&` range f `<=` set0 -> f @^-1` A = set0


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


6d4
6d5
x: R
~ range f x <-> f @^-1` [set x] = set0


711


713
f @^-1` [set x] = set0 -> ~ range f x

by apply: contraPnot => -[t _ <-] /seteqP[+ _] => /(_ t) /=.
Qed.


713
~ range f x -> f @^-1` [set x] = set0


71c
 by move/preimage10P. Qed.

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


aT, bT, rT: Type
f: aT -> bT -> rT
5e2
C, D: set bT
A `<=` B ->
C `<=` D ->
[set f x y | x in A & y in C]
`<=` [set f x y | x in B & y in D]


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


T1, T2, T3: Type
f: T1 -> T2
g: T2 -> T3
448
[set g x | x in [set f x | x in A]] =
[set (g \o f) x | x in A]


72a

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


c4
P: set (set T')
f: T -> T'
g: T' -> T
cancel f g ->
[set A | P [set f x | x in A]]
`<=` [set [set g x | x in A] | A in P]


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


735
cancel g f ->
[set [set g x | x in A] | A in P]
`<=` [set A | P [set f x | x in A]]


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


735
cancel f g ->
cancel g f ->
[set [set g x | x in A] | A in P] =
[set A | P [set f x | x in A]]


741

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


e5
[set Some x | x in set0] = set0


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


a1
[set Some x | x in [set x]] = [set Some x]


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


91
[set Some x | x in ~` A] =
[set~ None] `\` [set Some x | x in A]


750


91
[set~ None] `\` [set Some x | x in A]
`<=` [set Some x | x in ~` A]

by move=> [x [_ exAx]|[/(_ erefl)//]]; exists x => // Ax; apply: exAx; exists x.
Qed.


e5
range Some = [set~ None]


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


d3
[set Some x | x in A `&` B] =
[set Some x | x in A] `&` [set Some x | x in B]


75e


d3
[set Some x | x in A] `&` [set Some x | x in B]
`<=` [set Some x | x in A `&` B]

by move=> _ [[x + <-] [y By []]] => /[swap]<- Ay; exists y.
Qed.


d3
[set Some x | x in A `|` B] =
[set Some x | x in A] `|` [set Some x | x in B]


767

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


d3
[set Some x | x in A `\` B] =
[set Some x | x in A] `\` [set Some x | x in B]


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


d3
[set Some x | x in A] `<=` [set Some x | x in B] ->
A `<=` B


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


d3
[set Some x | x in A] `<=` [set Some x | x in B] <->
A `<=` B


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


d3
[set Some x | x in A] = [set Some x | x in B] -> A = B


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


91
[set Some x | x in A] = set0 <-> A = set0


780


91
[set Some x | x in A] = set0 -> A = set0

by rewrite -!subset0 => A0 x Ax; apply: (A0 (some x)); exists x.
Qed.


5b4
5b5
A: set rT
[set Some x | x in f @^-1` A] =
omap f @^-1` [set Some x | x in A]


789


78b
omap f @^-1` [set Some x | x in A]
`<=` [set Some x | x in f @^-1` A]

by move=> [x|] [a Aa //= [afx]]; exists x; rewrite // -afx.
Qed.


64d
[set Some x | x in [set f x | x in A]] =
[set omap f x | x in [set Some x | x in A]]


794
 by rewrite !image_comp. Qed.


d3
[disjoint
   [set Some x | x in A]
 & [set Some x | x in B]] = [disjoint A & B]


799

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

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


T, I: Type
6ce
46a
F: I -> set T
P i -> F i `<=` \bigcup_(j in P) F j


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


7a0
P i -> \bigcap_(j in P) F j `<=` F i


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


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


7ab


7a1
46a
F, G: I -> set T
FG: [set F i | i in P] `<=` [set G i | i in P]
26b
6ce
Pi: P i
Fit: F i t
([set F i | i in P] (F i) -> [set G i | i in P] (F i)) ->
(\bigcup_(i in P) G i) t

by move=> /(_ (ex_intro2 _ _ _ Pi erefl))[j Pj ji]; exists j => //; rewrite ji.
Qed.


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


7ba

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


7a1
46a
7b4
(forall i, P i -> F i = G i) ->
\bigcup_(i in P) F i = \bigcup_(i in P) G i


7bf

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


7c1
(forall i, P i -> F i = G i) ->
\bigcap_(i in P) F i = \bigcap_(i in P) G i


7c5

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


7a1
46a
7a2
~` (\bigcup_(i in P) F i) = \bigcap_(i in P) ~` F i


7ca

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


7cc
~` (\bigcap_(i in P) F i) = \bigcup_(i in P) ~` F i


7d0


7cc
\bigcap_(i in P) F i = \bigcap_(i in P) ~` ~` F i

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


T, I, rT: Type
46a
7a2
1c
[set f x | x in \bigcup_(i in P) F i] =
\bigcup_(i in P) [set f x | x in F i]


7d9


7db
\bigcup_(i in P) [set f x | x in F i]
`<=` [set f x | x in \bigcup_(i in P) F i]

by move=> _ [i Pi [x Fix <-]]; exists x => //; exists i.
Qed.


7cc
[set Some x | x in \bigcap_(i in P) F i] =
[set~ None]
`&` \bigcap_(i in P) [set Some x | x in F i]


7e4


7cc
[set Some x | x in \bigcap_(i in P) F i]
`<=` [set~ None]
     `&` \bigcap_(i in P) [set Some x | x in F i]
7cc
[set~ None]
`&` \bigcap_(i in P) [set Some x | x in F i]
`<=` [set Some x | x in \bigcap_(i in P) F i]

  
7cc
7ee

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


7cc
\bigcup_(i in P) F i = \bigcup_j F (val j)


7f3


7a1
46a
7a2
b
(\bigcup_(i in P) F i) x -> (\bigcup_j F (val j)) x

by move=> [i Pi Fix]; exists (SigSub (mem_set Pi)).
Qed.


7a1
P, Q: set I
7a2
P `<=>` Q ->
\bigcup_(i in P) F i = \bigcup_(i in Q) F i


7fd
 by move=> /seteqP->. Qed.


7ff
P `<=>` Q ->
\bigcap_(i in P) F i = \bigcap_(i in Q) F i


804
 by move=> /seteqP->. Qed.


7a1
800
7b4
P `<=>` Q ->
(forall i, P i -> F i = G i) ->
\bigcup_(i in P) F i = \bigcup_(i in Q) G i


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


80b
P `<=>` Q ->
(forall i, P i -> F i = G i) ->
\bigcap_(i in P) F i = \bigcap_(i in Q) G i


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


7c1
\bigcup_(i in P) (F i `|` G i) =
\bigcup_(i in P) F i `|` \bigcup_(i in P) G i


814

apply/predeqP => x; split=> [[i Pi [Fix|Gix]]|[[i Pi Fix]|[i Pi Gix]]];
  by [left; exists i|right; exists i|exists i =>//; left|exists i =>//; right].
Qed.


7c1
\bigcap_(i in P) (F i `&` G i) =
\bigcap_(i in P) F i `&` \bigcap_(i in P) G i


819


7c1
\bigcup_(i in P) ~` (F i `&` G i) =
\bigcup_(i in P) (~` F i `|` ~` G i)

by apply: eq_bigcupr => *; rewrite setCI.
Qed.


7a1
46a
a
P !=set0 -> \bigcup_(_ in P) A = A


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


824
P !=set0 -> \bigcap_(_ in P) A = A


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


7a1
46a
7a2
a
P !=set0 ->
\bigcap_(i in P) (F i `&` A) =
\bigcap_(i in P) F i `&` A


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


82f
P !=set0 ->
\bigcap_(i in P) (A `&` F i) =
A `&` \bigcap_(i in P) F i


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


82f
P !=set0 ->
\bigcup_(i in P) (F i `|` A) =
\bigcup_(i in P) F i `|` A


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


82f
P !=set0 ->
\bigcup_(i in P) (A `|` F i) =
A `|` \bigcup_(i in P) F i


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


7a1
7a2
\bigcup_(i in set0) F i = set0


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


7a1
7a2
6ce
\bigcup_(j in [set i]) F j = F i


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


844
\bigcap_(i in set0) F i = [set: T]


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


84a
\bigcap_(j in [set i]) F j = F i


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


7cc
\bigcup_(i in P) F i !=set0 <->
(exists2 i : I, P i & F i !=set0)


858

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


7cc
(forall i, P i -> F i = set0) ->
\bigcup_(i in P) F i = set0


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


7cc
(exists2 i : I, P i & F i = set0) ->
\bigcap_(i in P) F i = set0


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


7cc
(forall i, P i -> F i = [set: T]) ->
\bigcap_(i in P) F i = [set: T]


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


7cc
(exists2 i : I, P i & F i = [set: T]) ->
\bigcup_(i in P) F i = [set: T]


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


7cc
\bigcup_(i in P) F i = set0 <->
(forall i, P i -> F i = set0)


871


7a1
46a
7a2
F0: \bigcup_(i in P) F i `<=` set0
6ce
7b6
F i `<=` set0

by move=> t Ft; apply: F0; exists i.
Qed.


7cc
\bigcap_(i in P) F i = [set: T] <->
(forall i, P i -> F i = [set: T])


87c


7a1
46a
7a2
FT: [set: T] `<=` \bigcap_(i in P) F i
6ce
7b6
[set: T] `<=` F i

by move=> t _; apply: FT.
Qed.


7a1
7a2
46a
a
A `&` \bigcup_(i in P) F i =
\bigcup_(i in P) (A `&` F i)


887

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


889
\bigcup_(i in P) F i `&` A =
\bigcup_(i in P) (F i `&` A)


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


889
A `|` \bigcap_(i in P) F i =
\bigcap_(i in P) (A `|` F i)


892


889
\bigcup_(i in P) (~` A `&` ~` F i) =
\bigcup_(i in P) ~` (A `|` F i)

by under eq_bigcupr do rewrite -setCU.
Qed.


889
\bigcap_(i in P) F i `|` A =
\bigcap_(i in P) (F i `|` A)


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


7cc
\bigcup_(i in P) F i =
\bigcup_i (if i \in P then F i else set0)


8a0


7a1
46a
7a2
b
6ce
7b6
Fix: F i x
(\bigcup_i (if i \in P then F i else set0)) x
7a1
46a
7a2
b
6ce
(if i \in P then F i else set0) x ->
(\bigcup_(i in P) F i) x

  
8ac
8ad

by case: ifPn; rewrite (inE, notin_set) => Pi Fix; exists i.
Qed.


7ff
\bigcup_(i in P `&` Q) F i =
\bigcup_(i in P) (if i \in Q then F i else set0)


8b2


7a1
800
7a2
6ce
(if i \in P `&` Q then F i else set0) =
(if i \in P
 then if i \in Q then F i else set0
 else set0)

by rewrite in_setI; case: (i \in P) (i \in Q) => [] [].
Qed.


7ff
\bigcup_(i in P `&` Q) F i =
\bigcup_(i in Q) (if i \in P then F i else set0)


8bc


8b9
(if i \in P `&` Q then F i else set0) =
(if i \in Q
 then if i \in P then F i else set0
 else set0)

by rewrite in_setI; case: (i \in P) (i \in Q) => [] [].
Qed.


7a1
7a2
46a
\bigcap_(i in P) F i =
\bigcap_i (if i \in P then F i else [set: T])


8c5


7a1
7a2
46a
6ce
(if i \in P then ~` F i else set0) =
~` (if i \in P then F i else [set: T])

by case: ifP; rewrite ?setCT.
Qed.


7ff
\bigcap_(i in P `&` Q) F i =
\bigcap_(i in P) (if i \in Q then F i else [set: T])


8d0


8b9
(if i \in P `&` Q then F i else [set: T]) =
(if i \in P
 then if i \in Q then F i else [set: T]
 else [set: T])

by rewrite in_setI; case: (i \in P) (i \in Q) => [] [].
Qed.


7ff
\bigcap_(i in P `&` Q) F i =
\bigcap_(i in Q) (if i \in P then F i else [set: T])


8d9


8b9
(if i \in P `&` Q then F i else [set: T]) =
(if i \in Q
 then if i \in P then F i else [set: T]
 else [set: T])

by rewrite in_setI; case: (i \in P) (i \in Q) => [] [].
Qed.


7a1
46a
f: I -> T
\bigcup_(x in P) [set f x] = [set f x | x in P]


8e2

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


7a1
7a2
X, Y: set I
\bigcup_(i in (X `|` Y)) F i =
\bigcup_(i in X) F i `|` \bigcup_(i in Y) F i


8e9


7a1
7a2
8ec
26b
z: I
(X `|` Y) z ->
F z t ->
(\bigcup_(i in X) F i `|` \bigcup_(i in Y) F i) t
7a1
7a2
8ec
26b
(\bigcup_(i in X) F i `|` \bigcup_(i in Y) F i) t ->
(\bigcup_(i in (X `|` Y)) F i) t

  
8f7
8f8

by move=> [[z Xz Fzy]|[z Yz Fxz]]; exists z => //; [left|right].
Qed.


8eb
\bigcap_(i in (X `|` Y)) F i =
\bigcap_(i in X) F i `&` \bigcap_(i in Y) F i


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


7a1
7a2
x: I
X: set I
\bigcup_(i in (x |` X)) F i =
F x `|` \bigcup_(i in X) F i


902
 by rewrite bigcup_setU bigcup_set1. Qed.


904
\bigcap_(i in (x |` X)) F i =
F x `&` \bigcap_(i in X) F i


90a
 by rewrite bigcap_setU bigcap_set1. Qed.


7a1
905
7a2
906
X x ->
\bigcup_(i in X) F i =
F x `|` \bigcup_(i in X `\ x) F i


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


911
X x ->
\bigcap_(i in X) F i =
F x `&` \bigcap_(i in X `\ x) F i


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


T, I, U: Type
s: seq T
f: T -> set U
10c
~` (\big[setU/set0]_(t <- s | P t) f t) =
\big[setI/[set: U]]_(t <- s | P t) ~` f t


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


91c
~` (\big[setI/[set: U]]_(t <- s | P t) f t) =
\big[setU/set0]_(t <- s | P t) ~` f t


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


889
P !=set0 ->
\bigcap_(i in P) (A `\` F i) =
A `\` \bigcup_(i in P) F i


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


889
\bigcup_(i in P) F i `\` A =
\bigcup_(i in P) (F i `\` A)


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


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


932


935
936
46a
937
b
(\bigcup_(k in P `*`` Q) F k.1 k.2) x ->
(\bigcup_(i in P) \bigcup_(j in Q i) F i j) x

by move=> [[/= i j] [Pi Qj] Fijx]; exists i => //; exists j.
Qed.


935
936
46a
Q: set J
\bigcup_(i in P) \bigcup_(j in Q) F i j =
\bigcup_(k in P `*` Q) F k.1 k.2


940
 exact: bigcup_bigcup_dep. Qed.


7a1
Q: set I
7a2
46a
\bigcup_(i in P) F i =
\bigcup_(i in P `&` Q) F i
`|` \bigcup_(i in P `&` ~` Q) F i


947
 by rewrite -bigcup_setU -setIUr setUv setIT. Qed.


949
\bigcap_(i in P) F i =
\bigcap_(i in P `&` Q) F i
`&` \bigcap_(i in P `&` ~` Q) F i


94e
 by rewrite -bigcap_setU -setIUr setUv setIT. Qed.

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

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


d3
\bigcup_i bigcup2 A B i = A `|` B


953


9
b3
26b
(\bigcup_i bigcup2 A B i) t -> (A `|` B) t

by case=> -[_ At|[_ Bt|//]]; [left|right].
Qed.


d3
\bigcup_(i < 2) bigcup2 A B i = A `|` B


95d


95a
(\bigcup_(i < 2) bigcup2 A B i) t -> (A `|` B) t

by case=> -[_ At|[_ Bt|//]]; [left|right].
Qed.

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


d3
\bigcap_i bigcap2 A B i = A `&` B


966


d3
\bigcup_i
   ~`
   (if i == 0
    then A
    else if i == 1 then B else [set: T]) =
\bigcup_i
   (if i == 0
    then ~` A
    else if i == 1 then ~` B else set0)

by apply: eq_bigcupr => -[|[|[]]]//=; rewrite setCT.
Qed.


d3
\bigcap_(i < 2) bigcap2 A B i = A `&` B


96f


d3
\bigcup_(i < 2)
   ~`
   (if i == 0
    then A
    else if i == 1 then B else [set: T]) =
\bigcup_(i < 2)
   (if i == 0
    then ~` A
    else if i == 1 then ~` B else set0)

by apply: eq_bigcupr => // -[|[|[]]].
Qed.


7a1
7a2
65
46a
(forall i : I, P i -> F i `<=` D) ->
\bigcup_(i in P) F i `<=` D


978
 by move=> FD t [n Pn Fnt]; apply: (FD n). Qed.


97a
(forall i : I, P i -> D `<=` F i) ->
D `<=` \bigcap_(i in P) F i


97e
 by move=> DF t Dt n Pn; apply: DF. Qed.


7c1
(forall i : I, P i -> F i `<=` G i) ->
\bigcup_(i in P) F i `<=` \bigcup_(i in P) G i


983

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


7c1
(forall i : I, P i -> F i `<=` G i) ->
\bigcap_(i in P) F i `<=` \bigcap_(i in P) G i


988


7a1
46a
7b4
6ce
7b6
b
Fx: (\bigcap_(i in P) F i) x
F i x

exact: bigcap_inf Fx.
Qed.


6b7
P: set aT
f: aT -> I
6b8
\bigcup_(x in [set f x | x in P]) F x =
\bigcup_(x in P) F (f x)


993


6b7
996
997
6b8
681
(\bigcup_(x in P) F (f x)) x ->
(\bigcup_(x in [set f x | x in P]) F x) x

by case=> i Pi Ffix; exists (f i); [exists i|].
Qed.


I, T: Type
46a
7a2
\bigcap_(i in P) F i = \bigcap_j F (val j)


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


995
\bigcap_(x in [set f x | x in P]) F x =
\bigcap_(x in P) F (f x)


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


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


9ac


9af
9b0
9b1
9b2
IHX: forall Y : {fset I},
(Y `<` X)%fset -> \bigcup_(i in [set` Y]) F i = \big[setU/set0]_(i <- Y) F i
\bigcup_(i in [set` fset0]) F i =
\big[setU/set0]_(i <- fset0) F i
9af
9b0
9b1
9b2
9b9
905
xX: x \in X
9b3

  
9bd
9b3


9bd
\bigcup_(i in (x |` [set` (X `\ x)%fset])) F i =
F x `|` \big[setU/set0]_(i <- (X `\ x)%fset) F i

by rewrite bigcup_setU1 IHX// fproperD1.
Qed.


9ae
\bigcap_(i in [set` X]) F i =
\big[setI/[set: U]]_(i <- X) F i


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


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


9cc
 by rewrite set_fsetU1 bigcup_setU1. Qed.


9ce
\bigcap_(i in [set` (x |` X)%fset]) F i =
F x `&` \bigcap_(i in [set` X]) F i


9d5
 by rewrite set_fsetU1 bigcap_setU1. Qed.


9cf
b
9d0
9d1
x \in X ->
\bigcup_(i in [set` X]) F i =
F x `|` \bigcup_(i in [set` (X `\ x)%fset]) F i


9da
 by move=> Xx; rewrite (bigcup_setD1 x)// set_fsetD1. Qed.
Arguments bigcup_fsetD1 {T U} x.


9dc
x \in X ->
\bigcap_(i in [set` X]) F i =
F x `&` \bigcap_(i in [set` (X `\ x)%fset]) F i


9e0
 by move=> Xx; rewrite (bigcap_setD1 x)// set_fsetD1. Qed.
Arguments bigcup_fsetD1 {T U} x.

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


49e
9b0
91e
91f
10c
\bigcup_(t in [set x | (x \in s) && P x]) f t =
\big[setU/set0]_(t <- s | P t) f t


9e5


49e
9b0
91f
10c
4ad
91e
ih: \bigcup_(t in [set x | (x \in s) && P x]) f t =
\big[setU/set0]_(t <- s | P t) f t
\bigcup_(t in [set x | (x \in h :: s) && P x]) f t =
\big[setU/set0]_(t <- (h :: s) | P t) f t


49e
9b0
91f
10c
4ad
91e
9ee
u: U
26b
t \in h :: s ->
P t ->
f t u ->
(if P h
 then
  f h
  `|` \bigcup_(t in [set x | (x \in s) && P x]) f t
 else \bigcup_(t in [set x | (x \in s) && P x]) f t) u
49e
9b0
91f
10c
4ad
91e
9ee
9f4
(if P h
 then
  f h
  `|` \bigcup_(t in [set x | (x \in s) && P x]) f t
 else \bigcup_(t in [set x | (x \in s) && P x]) f t) u ->
(\bigcup_(t in [set x | (x \in h :: s) && P x]) f t) u


9f1
 
49e
9b0
91f
10c
4ad
91e
9ee
9f4
26b
ts: t \in s
Pt: P t
ftu: f t u
(if P h
 then
  f h
  `|` \bigcup_(t in [set x | (x \in s) && P x]) f t
 else \bigcup_(t in [set x | (x \in s) && P x]) f t) u
9f6

  
49e
9b0
91f
10c
4ad
91e
9ee
9f4
26b
9ff
a00
a01
Ph: ~~ P h
(\bigcup_(t in [set x | (x \in s) && P x]) f t) u
9f6

  
9f8
9f9


a0a
 
49e
9b0
91f
10c
4ad
91e
9ee
9f4
Ph: P h
fhu: f h u
(\bigcup_(t in [set x | (x \in h :: s) && P x]) f t) u
49e
9b0
91f
10c
4ad
91e
9ee
9f4
a11
26b
9ff
a00
a01
a13
49e
9b0
91f
10c
4ad
91e
9ee
9f4
a07
26b
9ff
a00
a01
a13

  
a0e
 
a16
a13
a17

  
a1b
 
a18
a13

  
a20
 by exists t => //; apply/andP; split => //; rewrite inE orbC ts.
Qed.


49e
9b0
91e
91f
\bigcup_(t in [set` s]) f t =
\big[setU/set0]_(t <- s) f t


a24


a26
(fun x : T => x \in s) =
(fun x : T => (x \in s) && true)

by rewrite funeqE => t; rewrite andbT.
Qed.


9e7
\bigcap_(t in [set x | (x \in s) && P x]) f t =
\big[setI/[set: U]]_(t <- s | P t) f t


a2e
 by apply: setC_inj; rewrite setC_bigcap setC_bigsetI bigcup_set_cond. Qed.


a26
\bigcap_(t in [set` s]) f t =
\big[setI/[set: U]]_(t <- s) f t


a33
 by apply: setC_inj; rewrite setC_bigcap setC_bigsetI bigcup_set. Qed.

End bigcup_set.


T: finType
9b0
577
91f
\bigcup_(t in [set` P]) f t =
\big[setU/set0]_(t in P) f t


a38


a3b
9b0
577
91f
9f4
(\big[setU/set0]_(t in P) f t) u ->
(\bigcup_(t in [set` P]) f t) u


a41
\big[orb/false]_(i in P) (u \in f i) ->
(\bigcup_(t in [set` P]) f t) u
a41
{morph (fun X : set_predType U => u \in X) : x y / 
x `|` y >-> x || y}
a41
(u \in set0) = false


a44
 
a41
a49
a4a


a4e
 
a41
a4b


a53
 by rewrite in_set0.
Qed.

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

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


9
C: set T -> Prop
G, X: set T
X `<=` G -> X `<=` smallest


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


9
a5a
G: set T
G `<=` smallest
 
a5f
 exact: sub_smallest. Qed.


a59
C X -> G `<=` X -> smallest `<=` X


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


a61
C G -> smallest = G


a6b

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

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


9
a5a
G1, G2: set T
C (smallest C G2) ->
G1 `<=` G2 -> smallest C G1 `<=` smallest C G2


a70
 by move=> *; apply: smallest_sub=> //; apply: sub_smallest. Qed.


9
C1, C2: set T -> Prop
(forall G : set T, C2 G -> C1 G) ->
forall G : set T, smallest C1 G `<=` smallest C2 G


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

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


9
4c5
F: nat -> set T
\bigcup_(i < n) F i = \big[setU/set0]_(i < n) F i


a7e


a80
\bigcup_(i < n) F i =
\bigcup_(t in [set` index_iota 0 n]) F t

by apply: eq_bigcupl; split=> i; rewrite /= mem_index_iota leq0n.
Qed.


a80
\bigcap_(i < n) F i = \big[setI/[set: T]]_(i < n) F i


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


9
i, n: nat
a81
i < n -> F i `<=` \big[setU/set0]_(j < n) F j


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


9
a81
4c5
\big[setU/set0]_(i < n) F i `<=` \bigcup_k F k


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


d3
\big[setU/set0]_(i < 2) bigcup2 A B i = A `|` B


a9b
 by rewrite -bigcup_mkord bigcup2inE. Qed.


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


aa0
 by rewrite -bigcap_mkord bigcap2inE. Qed.


a80
\bigcup_i F i =
\big[setU/set0]_(i < n) F i `|` \bigcup_i F (n + i)


aa5


a80
\bigcup_i F i =
\bigcup_(i in (`I_n `|` range (addn n))) F i


9
4c5
a81
k: nat
(`I_n `|` range (addn n)) k


9
4c5
a81
ab1
lenk: n <= k
range (addn n) k

by exists (k - n); rewrite // subnKC.
Qed.


a80
\bigcap_i F i =
\big[setI/[set: T]]_(i < n) F i
`&` \bigcap_i F (n + i)


aba

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


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


abf


9
a81
4e7
mn: m <= n
b
i: nat
im: `I_m i
8a8
(\bigcup_(i < n) F i) x

by exists i => //=; rewrite (leq_trans im).
Qed.


ac1
{homo (fun n : nat => \big[setI/[set: T]]_(i < n) F i) : n m / 
n <= m >-> m `<=` n}


acd


9
a81
4e7
ac8
\big[setU/set0]_t ~` F t `<=` \big[setU/set0]_t ~` F t

exact: (@subset_bigsetU (setC \o F)).
Qed.


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


ad7


9
ada
a81
n, m: nat
nm: n <= m
\big[setU/set0]_(i < n) (if P i then F i else set0)
`<=` \big[setU/set0]_(i < m) (if P i
                              then F i
                              else set0)

exact: (@subset_bigsetU (fun i => if P i then F i else _)).
Qed.


ad9
{homo (fun n : nat =>
       \big[setI/[set: T]]_(i < n | P i) F i) : n m / 
n <= m >-> m `<=` n}


ae5


ae0
\big[setI/[set: T]]_(i < m) (if P i
                             then F i
                             else [set: T])
`<=` \big[setI/[set: T]]_(i < n) (if P i
                                  then F i
                                  else [set: T])

exact: (@subset_bigsetI (fun i => if P i then F i else _)).
Qed.

End bigop_nat_lemmas.

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

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

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


49e
x0: T
P: set T
xget_spec x0 P (xget x0 P) (P (xget x0 P))


aee


49e
af1
af2
y:= xget x0 P: T
xget x0 P = y ->
xget_spec x0 P (xget x0 P) (P (xget x0 P))


49e
af1
af2
af9
_a_: exists x : T, `[< P x >]
(@sval) T (fun x : T => `[< P x >]) (sigW _a_) = y ->
xget_spec x0 P
  ((@sval) T (fun x : T => `[< P x >]) (sigW _a_))
  (P ((@sval) T (fun x : T => `[< P x >]) (sigW _a_)))
49e
af1
af2
af9
neqP: ~ (exists x : T, `[< P x >])
xget_spec x0 P x0 (P x0)

  
b03
b05


49e
af1
af2
af9
b04
b
~ P x

by apply: contra_not neqP => Px; exists x; apply/asboolP.
Qed.


af0
(exists x : T, P x) -> P (xget x0 P)


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


49e
af1
af2
b
P x -> P (xget x0 P)


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


b16
P x -> is_subset1 P -> xget x0 P = x


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


b16
P x -> (forall y : T, P y -> y = x) -> xget x0 P = x


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


af0
(forall x : T, ~ P x) -> xget x0 P = x0


b24
 by case: xgetP => // x _ Px /(_ x). Qed.

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


aT: Type
rT: choiceType
f: aT -> rT -> Prop
f0: aT -> rT
5b7
f a !=set0 -> f a (fun_of_rel f0 f a)


b29
 by move=> [b fab]; rewrite /fun_of_rel; apply: xgetI fab. Qed.


b2b
is_subset1 (f a) ->
forall b : rT, f a b -> fun_of_rel f0 f a = b


b33
 by move=> fa1 b /xget_subset1 xgeteq; rewrite /fun_of_rel xgeteq. Qed.


9
a
P: {x : T | x \in A} -> Prop
(forall u : {x : T | x \in A}, P u) =
(forall (u : T) (a : A u),
 P (exist (fun x : T => x \in A) u (mem_set a)))


b38


9
a
b3b
PA: forall (u : T) (a : A u),
P (exist (fun x : T => x \in A) u (mem_set a))
6c
a: u \in A
P (exist (fun x : T => x \in A) u a)


9
a
b3b
b42
6c
b43
Au: A u
b44

by rewrite (Prop_irrelevance a (mem_set Au)); apply: PA.
Qed.


9b0
A: set U
P: U -> Prop
{in A, forall x : U, P x} <->
(forall x : U, A x -> P x)


b4b
 by split=> AP x; have := AP x; rewrite inE. Qed.


U, V: Type
b4e
B: set V
P: U -> V -> Prop
{in A & B, forall (x : U) (y : V), P x y} <->
(forall (x : U) (y : V), A x -> B y -> P x y)


b53
 by split=> AP x y; have := AP x y; rewrite !inE. Qed.


T1: Type
P1: T1 -> Prop
{in [set: T1], forall x : T1, P1 x : Prop} ->
forall x : T1, P1 x : Prop


b5c
 by move=> + *; apply; rewrite !inE. Qed.


T1, T2: Type
P2: T1 -> T2 -> Prop
{in [set: T1] & [set: T2],
  forall (x : T1) (y : T2), P2 x y : Prop} ->
forall (x : T1) (y : T2), P2 x y : Prop


b64
 by move=> + *; apply; rewrite !inE. Qed.


72d
P3: T1 -> T2 -> T3 -> Prop
{in [set: T1] & [set: T2] & [set: T3],
  forall (x : T1) (y : T2) (z : T3), P3 x y z : Prop} ->
forall (x : T1) (y : T2) (z : T3), P3 x y z : Prop


b6c
 by move=> + *; apply; rewrite !inE. Qed.


b67
72e
{in [set: T1], bijective f} -> bijective f


b73
 by case=> [g /in1TT + /in1TT +]; exists g. Qed.

Module Pointed.

Definition point_of (T : Type) := T.

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

Section ClassDef.

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

Definition clone c of phant_id class c := @Pack T c.
Let xT := let: Pack T _ := cT in T.
Notation xclass := (class : class_of xT).
Local Coercion base : class_of >-> Choice.class_of.

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

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

End ClassDef.

Module Exports.

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

End Exports.

End Pointed.

Export Pointed.Exports.

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

Canonical arrow_pointedType (T : Type) (T' : pointedType) :=
  PointedType (T -> T') (fun=> point).

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

Canonical unit_pointedType := PointedType unit tt.
Canonical bool_pointedType := PointedType bool false.
Canonical Prop_pointedType := PointedType Prop False.
Canonical nat_pointedType := PointedType nat 0.
Canonical prod_pointedType (T T' : pointedType) :=
  PointedType (T * T') (point, point).
Canonical matrix_pointedType m n (T : pointedType) :=
  PointedType 'M[T]_(m, n) (\matrix_(_, _) point)%R.
Canonical option_pointedType (T : choiceType) := PointedType (option T) None.
Canonical pointed_fset {T : choiceType} := PointedType {fset T} fset0.

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

The format modifier has no effect for only-parsing
notations. [discarded-format-only-parsing,parsing]

Notation "[ 'get' x | E ]" := (get (fun x => E))
  (at level 0, x name, format "[ 'get'  x  |  E ]") : form_scope.

Section PointedTheory.
Context {T : pointedType}.


T: pointedType
af2
(exists x : T, P x) -> P [get x : _ | P x]


b7a
 exact: (xgetPex point). Qed.


b7d
af2
b
P x -> P [get x : _ | P x]


b81
 exact: (xgetI point). Qed.


b83
P x -> is_subset1 P -> [get x : _ | P x] = x


b87
 exact: (xget_subset1 point). Qed.


b83
P x ->
(forall y : T, P y -> y = x) -> [get x : _ | P x] = x


b8c
 exact: (xget_unique point). Qed.


b7c
(forall x : T, ~ P x) -> [get x : _ | P x] = point


b91
 exact: (xgetPN point). Qed.


b7d
[set: T] != set0 :> set T


b96
 by apply/eqP => /seteqP[] /(_ point) /(_ Logic.I). Qed.

End PointedTheory.

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

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

e5
cancel unsquash squash
 
b9c
 by move=> []. Qed.

(* Empty types *)

Module Empty.

Definition mixin_of T := T -> False.

Section EqMixin.
Variables (T : Type) (m : mixin_of T).
Definition eq_op (x y : T) := true.

9
m: mixin_of T
Equality.axiom eq_op
 
ba1
 by []. Qed.
Definition eqMixin := EqMixin eq_opP.
End EqMixin.

Section ChoiceMixin.
Variables (T : Type) (m : mixin_of T).
Definition find of pred T & nat : option T := None.

9
ba4
10c
4c5
b
find P n = Some x -> P x


ba8
 by []. Qed.

9
ba4
10c
(exists x : T, P x) -> exists n : nat, find P n


bae
 by case. Qed.

9
ba4
P, Q: pred T
P =1 Q -> find P =1 find Q


bb4
 by []. Qed.
Definition choiceMixin := Choice.Mixin findP ex_find eq_find.
End ChoiceMixin.

Section CountMixin.
Variables (T : Type) (m : mixin_of T).
Definition pickle : T -> nat := fun=> 0.
Definition unpickle : nat -> option T := fun=> None.

ba3
pcancel pickle unpickle
 
bbb
 by []. Qed.
Definition countMixin := CountMixin pickleK.
End CountMixin.

Section FinMixin.
Variables (T : countType) (m : mixin_of T).

T: countType
ba4
Finite.axiom ([::] : seq T)
 
bc0
 by []. Qed.
Definition finMixin := FinMixin fin_axiom.
End FinMixin.

Section ClassDef.

Set Primitive Projections.
Record class_of T := Class {
  base : Finite.class_of T;
  mixin : mixin_of T
}.
Unset Primitive Projections.
Local Coercion base : class_of >-> Finite.class_of.

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

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

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

End ClassDef.

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

New coercion path [mixin; eqMixin] : class_of >-> Equality.mixin_of is ambiguous with existing 
[base; Finite.base; Choice.base] : class_of >-> Equality.mixin_of.
[ambiguous-paths,typechecker]


New coercion path [mixin; choiceMixin] : class_of >-> Choice.mixin_of is ambiguous with existing 
[base; Finite.base; Choice.mixin] : class_of >-> Choice.mixin_of.
[ambiguous-paths,typechecker]


New coercion path [mixin; countMixin] : class_of >-> Countable.mixin_of is ambiguous with existing 
[base; Finite.mixin; Finite.mixin_base] : class_of >-> Countable.mixin_of.
[ambiguous-paths,typechecker]


New coercion path [mixin; eqMixin] : class_of >-> Equality.mixin_of is ambiguous with existing 
[base; Finite.base; Choice.base] : class_of >-> Equality.mixin_of.
[ambiguous-paths,typechecker]
New coercion path [mixin; choiceMixin] : class_of >-> Choice.mixin_of is ambiguous with existing 
[base; Finite.base; Choice.mixin] : class_of >-> Choice.mixin_of.
[ambiguous-paths,typechecker]
New coercion path [mixin; countMixin] : class_of >-> Countable.mixin_of is ambiguous with existing 
[base; Finite.mixin; Finite.mixin_base] : class_of >-> Countable.mixin_of.
[ambiguous-paths,typechecker]


End Empty.

New coercion path [Empty.mixin; Empty.eqMixin] : Empty.class_of >-> Equality.mixin_of is ambiguous with existing 
[Empty.base; Finite.base; Choice.base] : Empty.class_of >-> Equality.mixin_of.
[ambiguous-paths,typechecker]
New coercion path [Empty.mixin; Empty.choiceMixin] : Empty.class_of >-> Choice.mixin_of is ambiguous with existing 
[Empty.base; Finite.base; Choice.mixin] : Empty.class_of >-> Choice.mixin_of.
[ambiguous-paths,typechecker]
New coercion path [Empty.mixin; Empty.countMixin] : Empty.class_of >-> Countable.mixin_of is ambiguous with existing 
[Empty.base; Finite.mixin; Finite.mixin_base] : Empty.class_of >-> Countable.mixin_of.
[ambiguous-paths,typechecker]


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

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

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


T: emptyType
all_equal_to (set0 : set T)


bcc
 by move=> X; apply/setF_eq0/no. Qed.

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


T, C: Type
sort: C -> T
alt: emptyType -> T
(forall x : T,
 (exists y : emptyType, alt y = x) +
 (exists y : C, sort y = x)) ->
quasi_canonical_ sort alt


bd3
 by move=> + G Cx Gs x => /(_ x)[/cid[y <-]|/cid[y <-]]. Qed.
Arguments qcanon {T C sort alt} x.


quasi_canonical_ [eta Pointed.choiceType]
  [eta Empty.choiceType]


bdc


56b
((exists y : emptyType, y = T) +
 (exists y : pointedType, y = T))%type
49e
TF: T -> False
be3

  
be6
be3


be6
exists y : emptyType, y = T


49e
be7
cT:= CountType T (TF : Empty.mixin_of T): countType
bee


49e
be7
bf3
fM:= Empty.finMixin (TF : Empty.mixin_of cT): Finite.mixin_of cT
bee


bf7
EmptyType T TF = T

by case: T TF @cT @fM.
Qed.


quasi_canonical_ [eta Pointed.eqType]
  [eta Empty.eqType]


bfe

by apply: qcanon; elim/eqPchoice; elim/choicePpointed => [[T F]|T];
   [left; exists (Empty.Pack F) | right; exists T].
Qed.

quasi_canonical_ [eta Pointed.sort] [eta Empty.sort]


c03

by apply: qcanon; elim/Peq; elim/eqPpointed => [[T F]|T];
   [left; exists (Empty.Pack F) | right; exists T].
Qed.

Section partitions.

Definition trivIset T I (D : set I) (F : I -> set T) :=
  forall i j : I, D i -> D j -> F i `&` F j !=set0 -> i = j.


7a1
6c5
7a2
trivIset D F <->
trivIset [set: I]
  (fun i : I => if i \in D then F i else set0)


c08


7a1
6c5
7a2
tA: trivIset [set: I]
  (fun i : I => if i \in D then F i else set0)
i, j: I
Di: D i
Dj: D j
F i `&` F j !=set0 -> i = j
7a1
6c5
7a2
tA: trivIset D F
c12
(if i \in D then F i else set0)
`&` (if j \in D then F j else set0) !=set0 -> i = j

  
c18
c1a


7a1
6c5
7a2
c19
c12
iD: i \in D
F i `&` (if j \in D then F j else set0) !=set0 ->
i = j

by case: ifPn => [jD /tA|jD]; [apply; exact: set_mem|rewrite setI0 => -[]].
Qed.


9a3
6c5
trivIset D (fun=> set0 : set T)


c25
 by move=> i j Di Dj; rewrite setI0 => /set0P; rewrite eqxx. Qed.


9
I: eqType
6c5
7a2
trivIset D F <->
(forall i j : I,
 D i -> D j -> i != j -> F i `&` F j = set0)


c2b


9
c2e
6c5
7a2
tDF: forall i j : I, D i -> D j -> i != j -> F i `&` F j = set0
c12
c13
c14
c15

by move=> /set0P; apply: contraNeq => /tDF->.
Qed.


9
D: {pred nat}
a81
trivIset (fun x : nat => D x) F ->
forall n m : nat,
D m ->
n <= m ->
\big[setU/set0]_(i < n | D i) F i `&` F m = set0


c37


9
c3a
a81
tA: forall i j : nat_eqType,
D i -> D j -> i != j -> F i `&` F j = set0
m: nat
Dm: D m
0 <= m ->
\big[setU/set0]_(i < 0 | D i) F i `&` F m = set0
9
c3a
a81
c41
4c5
IHn: forall m : nat,
D m -> n <= m -> \big[setU/set0]_(i < n | D i) F i `&` F m = set0
c42
c43
n < m ->
\big[setU/set0]_(i < n.+1 | D i) F i `&` F m = set0

  
c47
c49


9
c3a
a81
c41
4c5
c48
c42
c43
lt_nm: n < m
(\big[setU/set0]_(i < n | D i) F i
 `|` (if D n then F n else set0)) `&` F m = set0


c50
(if D n then F n else set0) `&` F m = set0

by case: ifPn => [Dn|NDn]; rewrite ?set0I// tA// ltn_eqF.
Qed.


7a1
6c5
7b4
trivIset D F -> trivIset D (fun i : I => G i `&` F i)


c58

by move=> tF i j Di Dj [x [[Gix Fix] [Gjx Fjx]]]; apply tF => //; exists x.
Qed.


c5a
trivIset D F -> trivIset D (fun i : I => F i `&` G i)


c5e

by move=> tF i j Di Dj [x [[Fix Gix] [Fjx Gjx]]]; apply tF => //; exists x.
Qed.


9a3
D, D': set I
7a2
D `<=` D' -> trivIset D' F -> trivIset D F


c63
 by move=> DD' Ftriv i j /DD' + /DD' + /Ftriv->//. Qed.


d3
(A `&` B = set0) = trivIset [set: nat] (bigcup2 A B)


c6a


9
b3
AB0: A `&` B = set0
trivIset [set: nat] (bigcup2 A B)


c71
forall j : nat,
True ->
True ->
0 != j ->
A
`&` (if j == 0 then A else if j == 1 then B else set0) =
set0
c71
forall n j : nat,
True ->
True ->
n.+1 != j ->
(if n.+1 == 1 then B else set0)
`&` (if j == 0 then A else if j == 1 then B else set0) =
set0


c75
 
c71
c7a


c7d
 
c71
forall n : nat,
True ->
True ->
1 != n.+1 ->
(if 1 == 1 then B else set0)
`&` (if n.+1 == 0
     then A
     else if n.+1 == 1 then B else set0) = set0

  by move=> [//|j _ _ _]; rewrite setI0.
Qed.


T, I, I': Type
6c5
f: I -> I'
F: I' -> set T
trivIset D (F \o f) -> trivIset [set f x | x in D] F


c85

by move=> trivF i j [{}i Di <-] [{}j Dj <-] Ffij; congr (f _); apply: trivF.
Qed.
Arguments trivIset_image {T I I'} D f F.


c87
{in D &, injective f} ->
trivIset D (F \o f) = trivIset [set f x | x in D] F


c8e


c88
6c5
c89
c8a
finj: {in D &, injective f}
trivIset [set f x | x in D] F -> trivIset D (F \o f)


c88
6c5
c89
c8a
trivF: trivIset [set f x | x in D] F
c12
c13
c14
Ffij: (F \o f) i `&` (F \o f) j !=set0
f i = f j

by apply: trivF => //=; [exists i| exists j].
Qed.


5b4
D: set rT
5b5
trivIset D (fun x : rT => f @^-1` [set x])


ca0
 by move=> y z _ _ [x [<- <-]]. Qed.


b2c
b2d
ca3
5b6
5b5
trivIset D (fun x : rT => A `&` f @^-1` [set x])


ca7
 by move=> y z _ _ [x [[_ <-] [_ <-]]]. Qed.

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


c0a
cover D F = \bigcup_(i in D) F i


cad
 by []. Qed.


7a1
D', D: set I
7a2
D `<=` D' ->
(forall i : I, D' i -> ~ D i -> F i = set0) ->
cover D F = cover D' F


cb2


7a1
cb5
7a2
DD': D `<=` D'
D'DF: forall i : I, D' i -> ~ D i -> F i = set0
r: T
6ce
c13
Fit: F i r
(\bigcup_(i in D') F i) r
7a1
cb5
7a2
cbc
cbd
cbe
6ce
D'i: D' i
cbf
(\bigcup_(i in D) F i) r


cb9
 
cc3
cc5


cc8
 by have [Di|Di] := pselect (D i); [exists i | move: Fit; rewrite (D'DF i)].
Qed.


c5a
[set F i | i in D] = [set G i | i in D] ->
cover D F = cover D G


ccc


7a1
6c5
7b4
FG: [set F i | i in D] = [set G i | i in D]
cover D F = cover D G


7a1
6c5
7b4
cd4
26b
6ce
c13
7b7
cover D G t
7a1
6c5
7b4
cd4
26b
6ce
c13
Git: G i t
cover D F t

  
7a1
6c5
7b4
cd4
26b
6ce
c13
7b7
j: I
c14
GF: G j = F i
cda
cdb

  
cdd
cdf


7a1
6c5
7b4
cd4
26b
6ce
c13
cde
ce4
c14
GF: F j = G i
cdf

by exists j => //; rewrite GF.
Qed.

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

Definition pblock_index T (I : pointedType) D (F : I -> set T) (x : T) :=
  [get i | D i /\ F i x].

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

(* TODO: theory of trivIset, cover, partition, pblock_index and pblock *)

Notation trivIsets X := (trivIset X id).


c0a
trivIset D F -> trivIsets [set F i | i in D]


cef
 exact: trivIset_image. Qed.


cb4
D `<=` D' ->
(forall i : I, D' i -> ~ D i -> F i = set0) ->
trivIset D F = trivIset D' F


cf4


7a1
cb5
7a2
cbc
DD'F: forall i : I, D' i -> ~ D i -> F i = set0
trivIset D F = trivIset D' F


7a1
cb5
7a2
cbc
cfc
DF: trivIset D F
c12
cc4
D'j: D' j
FiFj0: F i `&` F j !=set0
i = j
7a1
cb5
7a2
cbc
cfc
D'F: trivIset D' F
c12
c13
c14
d04
d05

  
7a1
cb5
7a2
cbc
cfc
d02
c12
cc4
d03
d04
Di: ~ D i
d05
7a1
cb5
7a2
cbc
cfc
d02
c12
cc4
d03
d04
c13
d05
d07

    
d11
d05
d06

  
7a1
cb5
7a2
cbc
cfc
d02
c12
cc4
d03
d04
c13
c14
d05
7a1
cb5
7a2
cbc
cfc
d02
c12
cc4
d03
d04
c13
Dj: ~ D j
d05
d07

  
d16
 
d1b
d05
d06

  
d1f
 
d08
d05

by apply D'F => //; apply DD'.
Qed.


4a5
s1, s2: seq (set T)
D: set nat
`I_(size s1) `<=` D ->
perm_eq s1 s2 ->
trivIset D [eta nth set0 s1] ->
trivIset D [eta nth set0 s2]


d26


4a5
d29
d2a
s1D: `I_(size s1) `<=` D
s: seq nat_eqType
ss1: perm_eq s (iota 0 (size s1))
s12: s2 = [seq nth set0 s1 i | i <- s]
ts1: forall i j : nat_eqType,
D i -> D j -> i != j -> nth set0 s1 i `&` nth set0 s1 j = set0
trivIset D [eta nth set0 s2]


4a5
d29
d2a
d31
d32
d33
d34
d35
i, j: nat_eqType
c13
c14
ij: i != j
nth set0 s2 i `&` nth set0 s2 j = set0


4a5
s1: seq (set T)
d2a
d31
d32
d33
d35
d3b
c13
c14
d3c
si: size s <= i
nth set0 [seq nth set0 s1 i | i <- s] i
`&` nth set0 [seq nth set0 s1 i | i <- s] j = set0
4a5
d42
d2a
d31
d32
d33
d35
d3b
c13
c14
d3c
si: i < size s
d44

  
d47
d44


4a5
d42
d2a
d31
d32
d33
d35
d3b
c13
c14
d3c
d48
sj: size s <= j
nth set0 s1 (nth 0 s i)
`&` nth set0 [seq nth set0 s1 i | i <- s] j = set0
4a5
d42
d2a
d31
d32
d33
d35
d3b
c13
c14
d3c
d48
sj: j < size s
d51

  
d54
d51


4a5
d42
d2a
d31
d32
d33
d35
d3b
c13
c14
d3c
d48
d55
ab1
k < size s -> nth 0 s k \in iota 0 (size s1)
4a5
d42
d2a
d31
d32
d33
d35
d3b
c13
c14
d3c
d48
d55
nth_mem: forall k : nat,
k < size s -> nth 0 s k \in iota 0 (size s1)
d51

  
d60
d51


d60
`I_(size s1) (nth 0 s i)
4a5
d42
d2a
d31
d32
d33
ts1: forall i j : nat_eqType,
D i ->
D j ->
i != j -> nth set0 s1 i `&` nth set0 s1 j = set0
d3b
c13
c14
d3c
d48
d55
d61
`I_(size s1) (nth 0 s j)


d66
 
d60
d6d


d70
 by have := nth_mem _ sj; rewrite mem_iota leq0n add0n.
Qed.

End partitions.

#[deprecated(note="Use trivIset_setIl instead")]
Notation trivIset_setI := trivIset_setIl.

Definition total_on T (A : set T) (R : T -> T -> Prop) :=
  forall s t, A s -> A t -> R s t \/ R t s.

Section ZL.

Variable (T : Type) (t0 : T) (R : T -> T -> Prop).
Hypothesis (Rrefl : forall t, R t t).
Hypothesis (Rtrans : forall r s t, R r s -> R s t -> R r t).
Hypothesis (Rantisym : forall s t, R s t -> R t s -> s = t).
Hypothesis (tot_lub : forall A : set T, total_on A R -> exists t,
  (forall s, A s -> R s t) /\ forall r, (forall s, A s -> R s r) -> R t r).
Hypothesis (Rsucc : forall s, exists t, R s t /\ s <> t /\
  forall r, R s r -> R r t -> r = s \/ r = t).

Let Teq := @gen_eqMixin T.
Let Tch := @gen_choiceMixin T.
Let Tp := Pointed.Pack (Pointed.Class (Choice.Class Teq Tch) t0).
Let lub := fun A : {A : set T | total_on A R} =>
  [get t : Tp | (forall s, sval A s -> R s t) /\
    forall r, (forall s, sval A s -> R s r) -> R t r].
Let succ := fun s => [get t : Tp | R s t /\ s <> t /\
  forall r, R s r -> R r t -> r = s \/ r = t].

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


9
t0: T
R: T -> T -> Prop
Rrefl: forall t : T, R t t
Rtrans: forall r s t : T, R r s -> R s t -> R r t
Rantisym: forall s t : T, R s t -> R t s -> s = t
tot_lub: forall A : set T,
total_on A R ->
exists t : T,
  (forall s : T, A s -> R s t) /\
  (forall r : T,
   (forall s : T, A s -> R s r) -> R t r)
Rsucc: forall s : T,
exists t : T,
  R s t /\
  s <> t /\
  (forall r : T,
   R s r -> R r t -> r = s \/ r = t)
Teq:= gen_eqMixin: Equality.mixin_of T
Tch:= gen_choiceMixin: choiceMixin T
Tp:= Pointed.Pack
  {|
    Pointed.base :=
      {|
        Choice.base := Teq; Choice.mixin := Tch
      |};
    Pointed.mixin := t0
  |}: pointedType
lub:= fun A : {A : set T | total_on A R} =>
[get t : Tp | (forall s : T,
               (@sval) (set T)
                 ((total_on (T:=T))^~ R) A s ->
               R s t) /\
              (forall r : T,
               (forall s : T,
                (@sval) 
                  (set T) 
                  ((total_on (T:=T))^~ R) A s ->
                R s r) -> 
               R t r)]: {A : set T | total_on A R} -> Tp
succ:= fun s : T =>
[get t : Tp | R s t /\
              s <> t /\
              (forall r : T,
               R s r -> R r t -> r = s \/ r = t)]: T -> Tp
False


d74


9
d77
d78
d79
d7a
d7b
d7c
d7d
d7e
d7f
d80
d81
d82
A: {A : set T | total_on A R}
forall s : T,
(@sval) (set T) ((total_on (T:=T))^~ R) A s ->
R s (lub A)
9
d77
d78
d79
d7a
d7b
d7c
d7d
d7e
d7f
d80
d81
d82
lub_ub: forall (A : {A : set T | total_on A R})
  (s : T),
(@sval) (set T) ((total_on (T:=T))^~ R) A s ->
R s (lub A)
d83

  
d88
exists t : Tp,
  (forall s : T,
   (@sval) (set T) ((total_on (T:=T))^~ R) A s ->
   R s t) /\
  (forall r : T,
   (forall s : T,
    (@sval) (set T) ((total_on (T:=T))^~ R) A s ->
    R s r) -> R t r)
d8b

  
d8d
d83


9
d77
d78
d79
d7a
d7b
d7c
d7d
d7e
d7f
d80
d81
d82
d8e
d89
forall t : T,
(forall s : T,
 (@sval) (set T) ((total_on (T:=T))^~ R) A s -> R s t) ->
R (lub A) t
9
d77
d78
d79
d7a
d7b
d7c
d7d
d7e
d7f
d80
d81
d82
d8e
lub_lub: forall (A : {A : set T | total_on A R})
  (t : T),
(forall s : T,
 (@sval) (set T) ((total_on (T:=T))^~ R) A s ->
 R s t) -> R (lub A) t
d83

  
d99
d92
d9b

  
d9d
d83


9
d77
d78
d79
d7a
d7b
d7c
d7d
d7e
d7f
d80
d81
d82
d8e
d9e
s: T
R s (succ s) /\ s <> succ s
9
d77
d78
d79
d7a
d7b
d7c
d7d
d7e
d7f
d80
d81
d82
d8e
d9e
RS: forall s : T, R s (succ s) /\ s <> succ s
d83

  
dad
d83


9
d77
d78
d79
d7a
d7b
d7c
d7d
d7e
d7f
d80
d81
d82
d8e
d9e
dae
da9
forall t : T,
R s t -> R t (succ s) -> t = s \/ t = succ s
9
d77
d78
d79
d7a
d7b
d7c
d7d
d7e
d7f
d80
d81
d82
d8e
d9e
dae
succS: forall s t : T,
R s t -> R t (succ s) -> t = s \/ t = succ s
d83

  
db9
d83


9
d77
d78
d79
d7a
d7b
d7c
d7d
d7e
d7f
d80
d81
d82
d8e
d9e
dae
dba
Twtot: total_on tower R
d83
db9
total_on tower R

  
9
d77
d78
d79
d7a
d7b
d7c
d7d
d7e
d7f
d80
d81
d82
d8e
d9e
dae
dba
dc2
R_S: R
  (lub
     (exist ((total_on (T:=T))^~ R) tower Twtot))
  (succ
     (lub
        (exist ((total_on (T:=T))^~ R) tower
           Twtot)))
lub (exist ((total_on (T:=T))^~ R) tower Twtot) =
succ (lub (exist ((total_on (T:=T))^~ R) tower Twtot))
dc3

  
db9
dc5


9
d77
d78
d79
d7a
d7b
d7c
d7d
d7e
d7f
d80
d81
d82
d8e
d9e
dae
dba
d89
sATw: (@sval) (set T) ((total_on (T:=T))^~ R) A
`<=` tower
ihA: forall t : T,
(@sval) (set T) ((total_on (T:=T))^~ R) A t ->
forall t0 : T, tower t0 -> R t t0 \/ R t0 t
26b
Twt: tower t
R (lub A) t \/ R t (lub A)
9
d77
d78
d79
d7a
d7b
d7c
d7d
d7e
d7f
d80
d81
d82
d8e
d9e
dae
dba
da9
Tws: tower s
ihs: forall t : T, tower t -> R s t \/ R t s
26b
dd5
R (succ s) t \/ R t (succ s)

  
9
d77
d78
d79
d7a
d7b
d7c
d7d
d7e
d7f
d80
d81
d82
d8e
d9e
dae
dba
d89
dd3
dd4
26b
dd5
_a_: forall s : T,
(@sval) (set T) ((total_on (T:=T))^~ R) A s ->
R s t
dd6
dd2
`[< ~
    (forall s : T,
     (@sval) (set T) ((total_on (T:=T))^~ R) A s ->
     R s t) >] -> R (lub A) t \/ R t (lub A)
dd8

    
dd2
de4
dd7

  
9
d77
d78
d79
d7a
d7b
d7c
d7d
d7e
d7f
d80
d81
d82
d8e
d9e
dae
dba
d89
dd3
dd4
26b
dd5
da9
`[< ~
    ((@sval) (set T) ((total_on (T:=T))^~ R) A s ->
     R s t) >] -> R (lub A) t \/ R t (lub A)
dd7

  
9
d77
d78
d79
d7a
d7b
d7c
d7d
d7e
d7f
d80
d81
d82
d8e
d9e
dae
dba
d89
dd3
dd4
26b
dd5
da9
As: (@sval) (set T) ((total_on (T:=T))^~ R) A s
nRst: ~ R s t
R t (lub A)
dd7

  
dd9
ddc


9
d77
d78
d79
d7a
d7b
d7c
d7d
d7e
d7f
d80
d81
d82
d8e
d9e
dae
dba
da9
dda
ddb
26b
dd5
Rts: R t s
ddc
9
d77
d78
d79
d7a
d7b
d7c
d7d
d7e
d7f
d80
d81
d82
d8e
d9e
dae
dba
da9
dda
ddb
26b
dd5
RSst: R (succ s) t
ddc
dd9
forall r : T, tower r -> R r s \/ R (succ s) r

    
dfe
ddc
e00

  
dd9
e01


9
d77
d78
d79
d7a
d7b
d7c
d7d
d7e
d7f
d80
d81
d82
d8e
d9e
dae
dba
da9
dda
ddb
26b
dd5
d89
dd3
ihA: forall t : T,
(@sval) (set T) ((total_on (T:=T))^~ R) A t ->
R t s \/ R (succ s) t
R (lub A) s \/ R (succ s) (lub A)
9
d77
d78
d79
d7a
d7b
d7c
d7d
d7e
d7f
d80
d81
d82
d8e
d9e
dae
dba
da9
dda
ddb
26b
dd5
cbe
Twr: tower r
ihr: R r s \/ R (succ s) r
R (succ r) s \/ R (succ s) (succ r)

  
9
d77
d78
d79
d7a
d7b
d7c
d7d
d7e
d7f
d80
d81
d82
d8e
d9e
dae
dba
da9
dda
ddb
26b
dd5
d89
dd3
e0d
_a_: forall r : T,
(@sval) (set T) ((total_on (T:=T))^~ R) A r ->
R r s
e0e
e0c
`[< ~
    (forall r : T,
     (@sval) (set T) ((total_on (T:=T))^~ R) A r ->
     R r s) >] -> R (lub A) s \/ R (succ s) (lub A)
e10

    
e0c
e1c
e0f

  
9
d77
d78
d79
d7a
d7b
d7c
d7d
d7e
d7f
d80
d81
d82
d8e
d9e
dae
dba
da9
dda
ddb
26b
dd5
d89
dd3
e0d
cbe
`[< ~
    ((@sval) (set T) ((total_on (T:=T))^~ R) A r ->
     R r s) >] -> R (lub A) s \/ R (succ s) (lub A)
e0f

  
9
d77
d78
d79
d7a
d7b
d7c
d7d
d7e
d7f
d80
d81
d82
d8e
d9e
dae
dba
da9
dda
ddb
26b
dd5
d89
dd3
e0d
cbe
Ar: (@sval) (set T) ((total_on (T:=T))^~ R) A r
nRrs: ~ R r s
R (succ s) (lub A)
e0f

  
e11
e14


9
d77
d78
d79
d7a
d7b
d7c
d7d
d7e
d7f
d80
d81
d82
d8e
d9e
dae
dba
da9
dda
ddb
26b
dd5
cbe
e12
e13
Rrs: R r s
e14


e32
tower (succ r) -> R (succ r) s \/ R (succ s) (succ r)


9
d77
d78
d79
d7a
d7b
d7c
d7d
d7e
d7f
d80
d81
d82
d8e
d9e
dae
dba
da9
dda
ddb
26b
dd5
cbe
e12
e13
e33
RsSr: R s (succ r)
e14

by have [->|->] := succS _ _ Rrs RsSr; [right|left]; apply: Rrefl.
Qed.

End ZL.


9
d78
(forall t : T, R t t) ->
(forall r s t : T, R r s -> R s t -> R r t) ->
(forall s t : T, R s t -> R t s -> s = t) ->
(forall A : set T,
 total_on A R ->
 exists t : T, forall s : T, A s -> R s t) ->
exists t : T, forall s : T, R t s -> s = t


e3e


9
d78
d79
d7a
d7b
Rtot_max: forall A : set T,
total_on A R ->
exists t : T, forall s : T, A s -> R s t
exists t : T, forall s : T, R t s -> s = t


9
d78
d79
d7a
d7b
e47
totR:= {A : set T | total_on A R}: Type
e48


9
d78
d79
d7a
d7b
e47
e4d
R':= fun A B : totR =>
(@sval) (set T) ((total_on (T:=T))^~ R) A
`<=` (@sval) (set T) ((total_on (T:=T))^~ R) B: totR -> totR -> Prop
e48


9
d78
d79
d7a
d7b
e47
e4d
e52
R'refl: forall A : totR, R' A A
e48


9
d78
d79
d7a
d7b
e47
e4d
e52
e57
R'trans: forall A B C : totR,
R' A B -> R' B C -> R' A C
e48


9
d78
d79
d7a
d7b
e47
e4d
e52
e57
e5c
A, B: totR
R' A B -> R' B A -> A = B
9
d78
d79
d7a
d7b
e47
e4d
e52
e57
e5c
R'antisym: forall A B : totR,
R' A B -> R' B A -> A = B
e48

  
9
d78
d79
d7a
d7b
e47
e4d
e52
e57
e5c
B: set T
totB: total_on B R
a
totA: total_on A R
36b
sBA: B `<=` A
exist ((total_on (T:=T))^~ R) A totA =
exist ((total_on (T:=T))^~ R) B totB
e63

  
e65
e48


9
d78
d79
d7a
d7b
e47
e4d
e52
e57
e5c
e66
A: set totR
total_on A R' ->
exists t : totR,
  (forall s : totR, A s -> R' s t) /\
  (forall r : totR,
   (forall s : totR, A s -> R' s r) -> R' t r)
9
d78
d79
d7a
d7b
e47
e4d
e52
e57
e5c
e66
R'tot_lub: forall A : set totR,
total_on A R' ->
exists t : totR,
  (forall s : totR, A s -> R' s t) /\
  (forall r : totR,
   (forall s : totR, A s -> R' s r) ->
   R' t r)
e48

  
9
d78
d79
d7a
d7b
e47
e4d
e52
e57
e5c
e66
e77
Atot: total_on A R'
exists t : totR,
  (forall s : totR, A s -> R' s t) /\
  (forall r : totR,
   (forall s : totR, A s -> R' s r) -> R' t r)
e79

  
e80
total_on
  (\bigcup_(B in A)
      (@sval) (set T) ((total_on (T:=T))^~ R) B) R
9
d78
d79
d7a
d7b
e47
e4d
e52
e57
e5c
e66
e77
e81
AUtot: total_on
  (\bigcup_(B in A)
      (@sval) (set T) ((total_on (T:=T))^~ R)
        B) R
e82
e7a

    
9
d78
d79
d7a
d7b
e47
e4d
e52
e57
e5c
e66
e77
e81
s, t: T
B: totR
AB: A B
Bs: (@sval) (set T) ((total_on (T:=T))^~ R) B s
C: totR
AC: A C
Ct: (@sval) (set T) ((total_on (T:=T))^~ R) C t
R s t \/ R t s
e87

    
9
d78
d79
d7a
d7b
e47
e4d
e52
e57
e5c
e66
e77
e81
e8f
e90
e91
e92
e93
e94
e95
Cs: (@sval) (set T) ((total_on (T:=T))^~ R) C s
e96
9
d78
d79
d7a
d7b
e47
e4d
e52
e57
e5c
e66
e77
e81
e8f
e90
e91
e92
e93
e94
e95
Bt: (@sval) (set T) ((total_on (T:=T))^~ R) B t
e96
e88e7a

      
e9e
e96
e87

    
e89
e82
e79

  
e89
forall s : totR,
A s ->
R' s
  (exist ((total_on (T:=T))^~ R)
     (\bigcup_(B in A)
         (@sval) (set T) ((total_on (T:=T))^~ R) B)
     AUtot)
e89
forall r : totR,
(forall s : totR, A s -> R' s r) ->
R'
  (exist ((total_on (T:=T))^~ R)
     (\bigcup_(B in A)
         (@sval) (set T) ((total_on (T:=T))^~ R) B)
     AUtot) r
e7a

    
e89
eac
e79

  
e7b
e48


9
d78
d79
d7a
d7b
e47
e4d
e52
e57
e5c
e66
e7c
nomax: ~ (exists t : T, forall s : T, R t s -> s = t)
d83


9
d78
d79
d7a
d7b
e47
e4d
e52
e57
e5c
e66
e7c
eb7
26b
exists s : T, R t s /\ s <> t
9
d78
d79
d7a
d7b
e47
e4d
e52
e57
e5c
e66
e7c
nomax: forall t : T, exists s : T, R t s /\ s <> t
d83

  
ebb
~ (forall s : T, R t s -> s = t) ->
exists s : T, R t s /\ s <> t
ebd

  
9
d78
d79
d7a
d7b
e47
e4d
e52
e57
e5c
e66
e7c
eb7
t, s: T
~ (R t s -> s = t) -> exists s : T, R t s /\ s <> t
ebd

  
ebf
d83


9
d78
d79
d7a
d7b
e47
e4d
e52
e57
e5c
e66
e7c
ec0
tot0: total_on set0 R
d83


9
d78
d79
d7a
d7b
e47
e4d
e52
e57
e5c
e66
ec0
ed2
d89
exists t : {A : set T | total_on A R},
  R' A t /\
  A <> t /\
  (forall r : {A : set T | total_on A R},
   R' A r -> R' r t -> r = A \/ r = t)


9
d78
d79
d7a
d7b
e47
e4d
e52
e57
e5c
e66
ec0
ed2
d89
26b
tub: forall s : T,
(@sval) (set T) ((total_on (T:=T))^~ R) A s ->
R s t
da9
dfb
snet: s <> t
ed7


edb
total_on
  ((@sval) (set T) ((total_on (T:=T))^~ R) A
   `|` [set s]) R
9
d78
d79
d7a
d7b
e47
e4d
e52
e57
e5c
e66
ec0
ed2
d89
26b
edc
da9
dfb
edd
Astot: total_on
  ((@sval) (set T) ((total_on (T:=T))^~ R) A
   `|` [set s]) R
ed7

  
9
d78
d79
d7a
d7b
e47
e4d
e52
e57
e5c
e66
ec0
ed2
d89
26b
edc
da9
dfb
edd
u, v: T
((@sval) (set T) ((total_on (T:=T))^~ R) A `|` [set s])
  v -> R s v \/ R v s
9
d78
d79
d7a
d7b
e47
e4d
e52
e57
e5c
e66
ec0
ed2
d89
26b
edc
da9
dfb
edd
eea
Au: (@sval) (set T) ((total_on (T:=T))^~ R) A u
((@sval) (set T) ((total_on (T:=T))^~ R) A `|` [set s])
  v -> R u v \/ R v u
ee3

    
eee
ef0
ee2

  
eee
R u s
ee2

  
ee4
ed7


ee4
A <>
exist ((total_on (T:=T))^~ R)
  ((@sval) (set T) ((total_on (T:=T))^~ R) A
   `|` [set s]) Astot /\
(forall r : {A : set T | total_on A R},
 R' A r ->
 R' r
   (exist ((total_on (T:=T))^~ R)
      ((@sval) (set T) ((total_on (T:=T))^~ R) A
       `|` [set s]) Astot) ->
 r = A \/
 r =
 exist ((total_on (T:=T))^~ R)
   ((@sval) (set T) ((total_on (T:=T))^~ R) A
    `|` [set s]) Astot)


9
d78
d79
d7a
d7b
e47
e4d
e52
e57
e5c
e66
ec0
ed2
d89
26b
edc
da9
dfb
edd
ee5
AeAs: A =
exist ((total_on (T:=T))^~ R)
  ((@sval) (set T) ((total_on (T:=T))^~ R) A
   `|` [set s]) Astot
d83
9
d78
d79
d7a
d7b
e47
e4d
e52
e57
e5c
e66
ec0
ed2
d89
26b
edc
da9
dfb
edd
ee5
e6b
Btot: total_on B R
sAB: R' A (exist ((total_on (T:=T))^~ R) B Btot)
sBAs: R' (exist ((total_on (T:=T))^~ R) B Btot)
  (exist ((total_on (T:=T))^~ R)
     ((@sval) (set T) ((total_on (T:=T))^~ R) A
      `|` [set s]) Astot)
exist ((total_on (T:=T))^~ R) B Btot = A \/
exist ((total_on (T:=T))^~ R) B Btot =
exist ((total_on (T:=T))^~ R)
  ((@sval) (set T) ((total_on (T:=T))^~ R) A
   `|` [set s]) Astot

  
f02
~ (@sval) (set T) ((total_on (T:=T))^~ R) A s -> False
f04

  
f06
f0a


9
d78
d79
d7a
d7b
e47
e4d
e52
e57
e5c
e66
ec0
ed2
d89
26b
edc
da9
dfb
edd
ee5
e6b
f07
f08
f09
Bs: B s
f0a
9
d78
d79
d7a
d7b
e47
e4d
e52
e57
e5c
e66
ec0
ed2
d89
26b
edc
da9
dfb
edd
ee5
e6b
f07
f08
f09
nBs: ~ B s
f0a

  
f19
f0a


9
d78
d79
d7a
d7b
e47
e4d
e52
e57
e5c
e66
ec0
ed2
ec9
dfb
edd
e6b
f07
f1a
a
Atot: total_on A R
tub: forall s : T, A s -> R s t
Astot: total_on (A `|` [set s]) R
sBAs: R' (exist ((total_on (T:=T))^~ R) B Btot)
  (exist ((total_on (T:=T))^~ R)
     (A `|` [set s]) Astot)
sAB: R' (exist ((total_on (T:=T))^~ R) A Atot)
  (exist ((total_on (T:=T))^~ R) B Btot)
exist ((total_on (T:=T))^~ R) B Btot =
exist ((total_on (T:=T))^~ R) A Atot


9
d78
d79
d7a
d7b
e47
e4d
e52
e57
e5c
e66
ec0
ed2
ec9
dfb
edd
e6b
f07
f1a
a
f22
f23
f24
f25
f26
cbe
Br: B r
A r

by have /sBAs [|ser] // := Br; rewrite ser in Br.
Qed.

Definition premaximal T (R : T -> T -> Prop) (t : T) :=
  forall s, R t s -> R s t.


9
d77
d78
(forall t : T, R t t) ->
(forall r s t : T, R r s -> R s t -> R r t) ->
(forall A : set T,
 total_on A R ->
 exists t : T, forall s : T, A s -> R s t) ->
exists t : T, premaximal R t


f2f


9
d77
d78
d7e
d7f
f32


9
d77
d78
d7e
d7f
d80
f32


9
d77
d78
d7e
d7f
d80
d79
d7a
tot_max: forall A : set T,
total_on A R ->
exists t : T, forall s : T, A s -> R s t
exists t : T, premaximal R t


9
d77
d78
d7e
d7f
d80
d79
d7a
f40
eqR:= fun s t : T => R s t /\ R t s: T -> T -> Prop
ceqR:= fun s : T => [set t | eqR s t]: T -> set T
f41


9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
r, s, t: T
eqR r s -> eqR s t -> eqR r t
9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
eqR_trans: forall r s t : T,
eqR r s -> eqR s t -> eqR r t
f41

  
f50
f41


9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
f51
e8f
eqR s t -> ceqR s = ceqR t
9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
f51
ceqR_uniq: forall s t : T, eqR s t -> ceqR s = ceqR t
f41

  
f5c
f41


9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
f51
f5d
ceqRs:= range ceqR: set (set T)
quotR:= {x : set T | ceqRs x}: Type
f41


9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
f51
f5d
f65
f66
ceqRP: forall t : T, ceqRs (ceqR t)
f41


9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
f51
f5d
f65
f66
f6b
lift:= fun t : T => exist ceqRs (ceqR t) (ceqRP t): T -> {x : set T | ceqRs x}
f41


9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
f51
f5d
f65
f66
f6b
f70
A: quotR
exists t : Tp, lift t = A
9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
f51
f5d
f65
f66
f6b
f70
lift_surj: forall A : quotR,
exists t : Tp, lift t = A
f41

  
9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
f51
f5d
f65
f66
f6b
f70
a
26b
Tt: [set: T] t
exist ceqRs (ceqR t) (ceqRP t) =
exist ceqRs (ceqR t)
  (ex_intro2 [eta [set: T]]
     (fun x : T => ceqR x = ceqR t) t Tt
     (erefl (ceqR t)))
f77

  
f79
f41


9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
f51
f5d
f65
f66
f6b
f70
f7a
e8f
eqR s t -> lift s = lift t
9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
f51
f5d
f65
f66
f6b
f70
f7a
lift_inj: forall s t : T, eqR s t -> lift s = lift t
f41

  
f8b
f41


9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
f51
f5d
f65
f66
f6b
f70
f7a
f8c
e8f
lift s = lift t -> eqR s t
9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
f51
f5d
f65
f66
f6b
f70
f7a
f8c
lift_eqR: forall s t : T, lift s = lift t -> eqR s t
f41

  
9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
f51
f5d
f65
f66
f6b
f70
f7a
f8c
e8f
cst: lift s = lift t
ceqst: ceqR s = ceqR t
eqR s t
f95

  
f97
f41


9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
f51
f5d
f65
f66
f6b
f70
f7a
f8c
f98
repr:= fun A : quotR =>
[get x : _ | [set t | lift t = A] x]: quotR -> Tp
f41


9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
f51
f5d
f65
f66
f6b
f70
f7a
f8c
f98
fa7
repr_liftE: forall t : T, eqR t (repr (lift t))
f41


9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
f51
f5d
f65
f66
f6b
f70
f7a
f8c
f98
fa7
fac
R':= fun A B : quotR => R (repr A) (repr B): quotR -> quotR -> Prop
f41


9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
f51
f5d
f65
f66
f6b
f70
f7a
f8c
f98
fa7
fac
fb1
R'refl: forall A : quotR, R' A A
f41


9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
f51
f5d
f65
f66
f6b
f70
f7a
f8c
f98
fa7
fac
fb1
fb6
R'trans: forall A B C : quotR,
R' A B -> R' B C -> R' A C
f41


9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
f51
f5d
f65
f66
f6b
f70
f7a
f8c
f98
fa7
fac
fb1
fb6
fbb
A, B: quotR
e62
9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
f51
f5d
f65
f66
f6b
f70
f7a
f8c
f98
fa7
fac
fb1
fb6
fbb
R'antisym: forall A B : quotR,
R' A B -> R' B A -> A = B
f41

  
9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
f51
f5d
f65
f66
f6b
f70
f7a
f8c
f98
fa7
fac
fb1
fb6
fbb
fc0
RAB: R' A B
RBA: R' B A
t: Tp
tA: lift t = A
s: Tp
sB: lift s = B
dc
fc1

  
9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
f51
f5d
f65
f66
f6b
f70
f7a
f98
fa7
fac
fb1
fb6
fbb
fc0
fc9
fca
fcb
fcc
fcd
fce
eqR (repr (lift t)) s
fc1

  
9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
f51
f5d
f65
f66
f6b
f70
f7a
f98
fa7
fac
fb1
fb6
fbb
fc0
fc9
fca
fcb
fcc
fcd
fce
eAB: eqR (repr A) (repr B)
fd3
fc1

  
9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
f5d
f65
f66
f6b
f70
f7a
f98
fa7
fac
fb1
fb6
fbb
fc0
fc9
fca
fcb
fcc
fcd
fce
eqR (repr (lift s)) s
fc1

  
fc3
f41


9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
f51
f5d
f65
f66
f6b
f70
f7a
f8c
f98
fa7
fac
fb1
fb6
fbb
fc4
A: set quotR
e81
exists t : quotR, forall s : quotR, A s -> R' s t
9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
f51
f5d
f65
f66
f6b
f70
f7a
f8c
f98
fa7
fac
fb1
fb6
fbb
fc4
f75
Amax: forall s : quotR, R' A s -> s = A
f41

  
fe4
total_on [set repr B | B in A] R
9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
f51
f5d
f65
f66
f6b
f70
f7a
f8c
f98
fa7
fac
fb1
fb6
fbb
fc4
fe5
e81
26b
tmax: forall s : T, [set repr B | B in A] s -> R s t
fe6
fe8

    
ff1
fe6
fe7

  
9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
f51
f5d
f65
f66
f6b
f70
f7a
f8c
f98
fa7
fac
fb1
fb6
fbb
fc4
fe5
e81
26b
ff2
B: quotR
e91
Rt: R t (repr (lift t))
R' B (lift t)
fe7

  
fe9
f41


9
d77
d78
d7e
d7f
d80
d79
d7a
f40
f46
f47
f51
f5d
f65
f66
f6b
f70
f7a
f8c
f98
fa7
fac
fb1
fb6
fbb
fc4
f75
fea
26b
RAt: R (repr A) t
R t (repr A)


1003
R' A (lift t)
1003
R t (repr (lift t))

  
1003
100c

by have [] := repr_liftE t.
Qed.

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

Definition ubound A : set T := [set y | forall x, A x -> (x <= y)%O].
Definition lbound A : set T := [set y | forall x, A x -> (y <= x)%O].


1a
T: porderType d
a
b
(forall y, A y -> (y <= x)%O) <-> ubound A x


1011
 by []. Qed.


1013
(forall y, A y -> (x <= y)%O) <-> lbound A x


1018
 by []. Qed.


1a
1014
x, y: T
ubound [set x] y = (x <= y)%O


101d
 by rewrite propeqE; split => [/(_ x erefl)//|xy z ->]. Qed.


101f
lbound [set x] y = (y <= x)%O


1024
 by rewrite propeqE; split => [/(_ x erefl)//|xy z ->]. Qed.


101f
lbound (ubound [set x]) y -> (y <= x)%O


1029
 by move/(_ x); apply; rewrite ub_set1. Qed.


101f
ubound (lbound [set x]) y -> (x <= y)%O


102e
 by move/(_ x); apply; rewrite lb_set1. Qed.


1a
1014
b
lbound (ubound [set x]) x


1033
 by move=> y; apply. Qed.


1035
ubound (lbound [set x]) x


1039
 by move=> y; apply. Qed.


1a
1014
a
1020
ubound A y -> lbound (ubound A) x -> (x <= y)%O


103e
 by move=> Ay; apply. Qed.


1040
lbound A y -> ubound (lbound A) x -> (y <= x)%O


1044
 by move=> Ey; apply. Qed.

(* down set (i.e., generated order ideal) *)
(* i.e. down A := { x | exists y, y \in A /\ x <= y} *)
Definition down A : set T := [set x | exists y, A y /\ (x <= y)%O].

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


1035
has_ubound [set x]


1049
 by exists x; rewrite ub_set1. Qed.


1a
1014
~ has_inf set0


104e
 by rewrite /has_inf not_andP; left; apply/set0P/negP/negPn. Qed.


1050
~ has_sup set0


1054
 by rewrite /has_sup not_andP; left; apply/set0P/negP/negPn. Qed.


1035
has_sup [set x]


1059
 by split; [exists x | exists x => y ->]. Qed.


1035
has_inf [set x]


105e
 by split; [exists x | exists x => y ->]. Qed.


1a
1014
b3
A `<=` B -> has_lbound B -> has_lbound A


1063
 by move=> AB [l Bl]; exists l => a Aa; apply/Bl/AB. Qed.


1065
A `<=` B -> has_ubound B -> has_ubound A


1069
 by move=> AB [l Bl]; exists l => a Aa; apply/Bl/AB. Qed.


1013
(exists2 y : T, A y & (x <= y)%O) <-> down A x


106e
 by split => [[y Ay xy]|[y [Ay xy]]]; [exists y| exists y]. Qed.

Definition isLub A m := ubound A m /\ forall b, ubound A b -> (m <= b)%O.

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


1035
supremums [set x] = [set x]


1073


1035
(ubound [set x] `&` lbound (ubound [set x])) x
101f
ubound [set x] y ->
lbound (ubound [set x]) y -> [set x] y

  
101f
107d

by rewrite ub_set1 => xy /lb_ub_set1 yx; apply/eqP; rewrite eq_le xy yx.
Qed.


1a
1014
a
is_subset1 (supremums A)


1082


1a
1014
a
1020
Ax: ubound A x
xA: lbound (ubound A) x
Ay: ubound A y
yA: lbound (ubound A) y
x == y

by rewrite eq_le (ub_lb_ub Ax yA) (ub_lb_ub Ay xA).
Qed.

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


1a
1014
af1
a
~ has_sup A -> supremum x0 A = x0


1091


1a
1014
af1
a
hsA: ~ has_sup A
b
Ax: A x
xget x0 (supremums A) = x0


1a
1014
af1
a
109a
b
109b
uA: ubound A (xget x0 (supremums A))
d83

by apply: hsA; split; [exists x|exists (xget x0 (supremums A))].
Qed.


1a
1014
af1
supremum x0 set0 = x0


10a3
 by rewrite /supremum eqxx. Qed.


1a
1014
x0, x: T
supremum x0 [set x] = x


10a9


10ab
([set x] == set0) = false
10ab
xget x0 (supremums [set x]) = x

  
10ab
10b5

by rewrite supremums1; case: xgetP => // /(_ x) /(_ erefl).
Qed.

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


1035
infimums [set x] = [set x]


10ba


1035
(lbound [set x] `&` ubound (lbound [set x])) x
101f
lbound [set x] y ->
ubound (lbound [set x]) y -> [set x] y

  
101f
10c4

by rewrite lb_set1 => xy /ub_lb_set1 yx; apply/eqP; rewrite eq_le xy yx.
Qed.


1084
is_subset1 (infimums A)


10c9


1a
1014
a
1020
Ax: lbound A x
xA: ubound (lbound A) x
Ay: lbound A y
yA: ubound (lbound A) y
108f

by rewrite eq_le (lb_ub_lb Ax yA) (lb_ub_lb Ay xA).
Qed.

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

End UpperLowerTheory.

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


1a
T: orderType d
af1
a
26b
supremums A !=set0 -> A t -> (t <= supremum x0 A)%O


10d6


1a
10d9
af1
a
t, x: T
Ax: supremums A x
A t -> (t <= xget x0 (supremums A))%O

by case: xgetP => [y yA [uAy _]|/(_ x) //]; exact: uAy.
Qed.


10d8
infimums A !=set0 -> A t -> (infimum x0 A <= t)%O


10e4


1a
10d9
af1
a
10e0
Ex: infimums A x
A t -> (xget x0 (infimums A) <= t)%O

by case: xgetP => [y yE [uEy _]|/(_ x) //]; exact: uEy.
Qed.

End UpperLowerOrderTheory.


A: set nat
ubound A !=set0 -> supremums A !=set0


10ef


10f2
4c5
ih: ubound A n -> supremums A !=set0
ubound A n.+1 -> supremums A !=set0


10f2
4c5
An: ~ ubound A n
An1: ubound A n.+1
supremums A !=set0


10f2
4c5
1100
m: Order.NatOrder.porderType
Am: ubound A m
k: Order.NatOrder.porderType
Ak: A k
~~ (k <= n)%O -> (n.+1 <= m)%O


10f2
4c5
1100
1106
1107
1108
1109
kn: (n < k)%O
(n.+1 <= m)%O

by rewrite (Order.POrderTheory.le_trans _ (Am _ Ak)).
Qed.

Definition meets T (F G : set (set T)) :=
  forall A B, F A -> G B -> A `&` B !=set0.

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

Section meets.


9
F, G: set (set T)
F `#` G = G `#` F


1112


1114
F `#` G -> G `#` F
9
1115
sFG: forall F G : set (set T), F `#` G -> G `#` F
1116

  
111e
1116

by rewrite propeqE; split; apply: sFG.
Qed.


9
F, F', G, G': set (set T)
F `<=` F' -> G `<=` G' -> F' `#` G' -> F `#` G


1124
 by move=> sF sG FG A B /sF FA /sG GB; apply: (FG A B). Qed.


9
F, G, G': set (set T)
G `<=` G' -> F `#` G' -> F `#` G


112b
 exact: sub_meets. Qed.


9
G, F, F': set (set T)
F `<=` F' -> F' `#` G -> F `#` G


1132
 by move=> /sub_meets; apply. Qed.

End meets.


unit
 
1139
 by []. Qed.

Module SetOrder.
Module Internal.
Section SetOrder.

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


d3
`[< A `<=` B >] = (A `&` B == A)


113e
 by apply/asboolP/eqP; rewrite setIidPl. Qed.


d3
`[< A `<` B >] = (B != A) && `[< A `<=` B >]


1143

apply/idP/idP => [/asboolP|/andP[BA /asboolP AB]]; rewrite properEneq eq_sym;
  by [move=> [] -> /asboolP|apply/asboolP].
Qed.


9
B, A: set T
A `&` (A `|` B) = A


1148
 by rewrite setUC setKU. Qed.


114a
A `|` A `&` B = A


114f
 by rewrite setIC setKI. Qed.

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

Local Canonical porderType := POrderType set_display (set T) orderMixin.
Local Canonical latticeType := LatticeType (set T) orderMixin.
Local Canonical distrLatticeType := DistrLatticeType (set T) orderMixin.


91
(set0 <= A)%O


1154
 by apply/asboolP; apply: sub0set. Qed.


91
(A <= [set: T])%O


1159
 exact/asboolP. Qed.

Local Canonical bLatticeType :=
  BLatticeType (set T) (Order.BLattice.Mixin SetOrder_sub0set).
Local Canonical tbLatticeType :=
  TBLatticeType (set T) (Order.TBLattice.Mixin SetOrder_setTsub).
Local Canonical bDistrLatticeType := [bDistrLatticeType of set T].
Local Canonical tbDistrLatticeType := [tbDistrLatticeType of set T].


d3
B `&` (A `\` B) = set0


115e
 by rewrite setDE setICA setICr setI0. Qed.


42c

42f by rewrite setUC -setDDr setDv setD0. Qed.

Local Canonical cbDistrLatticeType := CBDistrLatticeType (set T)
  (@CBDistrLatticeMixin _ _ (fun A B => A `\` B) subKI joinIB).

Local Canonical ctbDistrLatticeType := CTBDistrLatticeType (set T)
  (@CTBDistrLatticeMixin _ _ _ (fun A => ~` A) (fun x => esym (setTD x))).

End SetOrder.
End Internal.

Module Exports.

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

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


d3
(A <= B)%O = (A `<=` B)


1164
 by rewrite asboolE. Qed.


d3
(A < B)%O = (A `<` B)


1169
 by rewrite asboolE. Qed.


d3
(A `\` B)%O = A `\` B
 
116e
 by []. Qed.


91
(~` A)%O = ~` A
 
1173
 by []. Qed.


e5
0%O = set0
 
1178
 by []. Qed.


e5
1%O = [set: T]
 
117d
 by []. Qed.


d3
(A `&` B)%O = A `&` B
 
1182
 by []. Qed.


d3
(A `|` B)%O = A `|` B
 
1187
 by []. Qed.


d3
reflect (A `<=` B) (A <= B)%O


118c
 by apply: (iffP idP); rewrite subsetEset. Qed.


d3
reflect (A `<` B) (A < B)%O


1191
 by apply: (iffP idP); rewrite properEset. Qed.

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

Section product.
Variables (T1 T2 : Type).
Implicit Type A B : set (T1 * T2).


b67
{homo fst_set (T2:=T2) : A B / A `<=` B >-> A `<=` B}


1196
 by move=> A B AB x [y Axy]; exists y; exact/AB. Qed.


1198
{homo snd_set (T2:=T2) : A B / A `<=` B >-> A `<=` B}


119c
 by move=> A B AB x [y Axy]; exists y; exact/AB. Qed.


b67
A: set (T1 * T2)
A `<=` A.`1 \o fst
 
11a1
 by move=> [x y]; exists y. Qed.


11a3
A `<=` A.`2 \o snd
 
11a8
 by move=> [x y]; exists x. Qed.


b67
X: set T1
Y: set T2
(X `*` Y).`1 `<=` X


11ad
 by move=> x [y [//]]. Qed.


11af
(X `*` Y).`2 `<=` Y


11b5
 by move=> x [y [//]]. Qed.


b67
11b0
Y: T1 -> set T2
(X `*`` Y).`1 `<=` X


11ba
 by move=> x [y [//]]. Qed.

End product.

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

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

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


b67
11a4
471
xsection A x `<=` A.`2


11c1
 by move=> y Axy; exists x; rewrite /xsection/= inE in Axy. Qed.


b67
11a4
472
ysection A y `<=` A.`1


11c7
 by move=> x Axy; exists y; rewrite /ysection/= inE in Axy. Qed.


b67
471
472
11a4
(y \in xsection A x) = ((x, y) \in A)


11cd
 by apply/idP/idP => [|]; [rewrite inE|rewrite /xsection !inE /= inE]. Qed.


11cf
(x \in ysection A y) = ((x, y) \in A)


11d3
 by apply/idP/idP => [|]; [rewrite inE|rewrite /ysection !inE /= inE]. Qed.


b67
471
xsection set0 x = set0


11d8
 by rewrite predeqE /xsection => y; split => //=; rewrite inE. Qed.


b67
472
ysection set0 y = set0


11de
 by rewrite predeqE /ysection => x; split => //=; rewrite inE. Qed.


b67
X1: set_predType T1
457
471
x \in X1 -> xsection (X1 `*` X2) x = X2


11e4


b67
11e7
457
471
xX1: x \in X1
X2 `<=` xsection (X1 `*` X2) x

by move=> y X2y; rewrite /xsection/= inE; split=> //=; rewrite inE in xX1.
Qed.


b67
456
X2: set_predType T2
472
y \in X2 -> ysection (X1 `*` X2) y = X1


11f1


b67
456
11f4
472
yX2: y \in X2
X1 `<=` ysection (X1 `*` X2) y

by move=> x X1x; rewrite /ysection/= inE; split=> //=; rewrite inE in yX2.
Qed.


11e6
x \notin X1 -> xsection (X1 `*` X2) x = set0


11fe


b67
11e7
457
471
xX1: x \notin X1
472
[set y | (x, y) \in X1 `*` X2] y -> set0 y

by rewrite /xsection/= inE => -[] /=; rewrite notin_set in xX1.
Qed.


11f3
y \notin X2 -> ysection (X1 `*` X2) y = set0


1209


b67
456
11f4
472
yX2: y \notin X2
471
ysection (X1 `*` X2) y x -> set0 x

by rewrite /ysection/= inE => -[_]; rewrite notin_set in yX2.
Qed.


b67
F: nat -> set (T1 * T2)
471
xsection (\bigcup_n F n) x =
\bigcup_n xsection (F n) x


1214


b67
1217
471
472
(\bigcup_n F n) (x, y) ->
(\bigcup_n [set y | (x, y) \in F n]) y
b67
1217
471
472
4c5
F n (x, y) -> (x, y) \in \bigcup_n F n

  
1221
1222

by move=> Fnxy; rewrite inE; exists n.
Qed.


b67
1217
472
ysection (\bigcup_n F n) y =
\bigcup_n ysection (F n) y


1227


b67
1217
472
471
(\bigcup_n F n) (x, y) ->
(\bigcup_n [set x | (x, y) \in F n]) x
b67
1217
472
471
4c5
1222

  
1233
1222

by move=> Fnxy; rewrite inE; exists n.
Qed.


1216
trivIset [set: nat] F ->
trivIset [set: nat] (fun n : nat => xsection (F n) x)


1238


b67
1217
471
h: forall i j : nat_eqType,
[set: nat] i ->
[set: nat] j -> i != j -> F i `&` F j = set0
d3b
d3c
xsection (F i) x `&` xsection (F j) x = set0


b67
1217
471
1240
d3b
d3c
472
Fixy: F i (x, y)
Fjxy: F j (x, y)
d83

by have := h i j Logic.I Logic.I ij; rewrite predeqE => /(_ (x, y))[+ _]; apply.
Qed.


1229
trivIset [set: nat] F ->
trivIset [set: nat] (fun n : nat => ysection (F n) y)


1249


b67
1217
472
1240
d3b
d3c
ysection (F i) y `&` ysection (F j) y = set0


b67
1217
472
1240
d3b
d3c
471
1246
1247
d83

by have := h i j Logic.I Logic.I ij; rewrite predeqE => /(_ (x, y))[+ _]; apply.
Qed.


11da
{homo xsection^~ x : X Y / X `<=` Y >-> X `<=` Y}


1257
 by move=> X Y XY y; rewrite /xsection /= 2!inE => /XY. Qed.


11e0
{homo ysection^~ y : X Y / X `<=` Y >-> X `<=` Y}


125c
 by move=> X Y XY x; rewrite /ysection /= 2!inE => /XY. Qed.


b67
A, B: set (T1 * T2)
471
xsection (A `&` B) x = xsection A x `&` xsection B x


1261
 by rewrite /xsection predeqE => y/=; split; rewrite !inE => -[]. Qed.


b67
1264
472
ysection (A `&` B) y = ysection A y `&` ysection B y


1268
 by rewrite /ysection predeqE => x/=; split; rewrite !inE => -[]. Qed.


b67
X, Y: set (T1 * T2)
471
xsection (X `\` Y) x = xsection X x `\` xsection Y x


126e
 by rewrite predeqE /xsection /= => y; split; rewrite !inE. Qed.


b67
1271
472
ysection (X `\` Y) y = ysection X y `\` ysection Y y


1275
 by rewrite predeqE /ysection /= => x; split; rewrite !inE. Qed.


b67
44f
471
xsection (snd @^-1` B) x = B


127b
 by apply/seteqP; split; move=> y/=; rewrite /xsection/= inE. Qed.


b67
448
472
ysection (fst @^-1` A) y = A


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

End section.

Notation "B \; A" :=
  ([set xy | exists2 z, A (xy.1, z) & B (z, xy.2)]) : classical_set_scope.


X, Y: Type
A, C: set (X * Y)
B, D: set (Y * X)
A `<=` C -> B `<=` D -> A \; B `<=` C \; D


1287

by move=> AsubC BD [x z] /= [y] Bxy Ayz; exists y; [exact: BD | exact: AsubC].
Qed.


X: Type
E: set (X * X)
E \; range (fun x : X => (x, x)) = E


1290


1293
1294
x, y: X
Exy: E (x, y)
exists2 z : X,
  exists2 x0 : X, True & (x0, x0) = (x, z) & E (z, y)

by exists x => //; exists x.
Qed.