Library mathcomp.analysis.classical_sets
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From mathcomp Require Import all_ssreflect ssralg matrix finmap order.
From mathcomp Require Import ssrnum ssrint interval.
Require Import boolp.
From mathcomp Require Import all_ssreflect ssralg matrix finmap order.
From mathcomp Require Import ssrnum ssrint interval.
Require Import boolp.
This file develops a basic theory of sets and types equipped with a
canonical inhabitant (pointed types).
--> A decidable equality is defined for any type. It is thus possible to
define an eqType structure for any type using the mixin gen_eqMixin.
> This file adds the possibility to define a choiceType structure for
any type thanks to an axiom gen_choiceMixin giving a choice mixin.
> We chose to have generic mixins and no global instances of the eqType
and choiceType structures to let the user choose which definition of
equality to use and to avoid conflict with already declared instances.
About the naming conventions in this file:
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. [set of F] == set defined by the expression F x for any x. [set a] == set containing only a. [set a : T] == same as before with the type of a made explicit. A `|` B == union of A and B. a |` A == A extended with a. [set a1; a2; ..; an] == set containing only the n elements ai. A `&` B == intersection of A and B. A `*` B == product of A and B, i.e. set of pairs (a,b) such that A a and B b. A.`1 == set of points a such that there exists b so that A (a, b). A.`2 == set of points a such that there exists b so that A (b, a). ~` A == complement of A. [set~ a] == complement of [set a]. A `\` B == complement of B in A. A `\ a == A deprived of a. \bigcup(i in P) F == union of the elements of the family F whose index satisfies P. \bigcup(i : T) F == union of the family F indexed on T. \bigcup_i F == same as before with T left implicit. \bigcap(i in P) F == intersection of the elements of the family F whose index satisfies P. \bigcap(i : T) F == union of the family F indexed on T. \bigcap_i F == same as before with T left implicit. 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[ ] 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.Upper and lower bounds:
ubound, lbound == upper bound and lower bound sets supremum x0 E == supremum of E or x0 if E is empty- use T, T', T1, T2, etc., aT (domain type), rT (return type) for names of variables in Type (or choiceType/pointedType/porderType) + use the same suffix or prefix for the sets as their containing type (e.g., A1 in T1, etc.) + as a consequence functions are rather of type aT -> rT
- use I, J when the type corresponds to an index
- sets are named A, B, C, D, etc., or Y when it is ostensibly an image set (i.e., of type set rT)
- indexed sets are rather named F
Set Implicit Arguments.
Declare Scope classical_set_scope.
Reserved Notation "[ 'set' x : T | P ]"
(at level 0, x at level 99, only parsing).
Reserved Notation "[ 'set' x | P ]"
(at level 0, x, P at level 99, format "[ 'set' x | P ]").
Reserved Notation "[ 'set' E | x 'in' A ]" (at level 0, E, x at level 99,
format "[ '[hv' 'set' E '/ ' | x 'in' A ] ']'").
Reserved Notation "[ 'set' E | x 'in' A & y 'in' B ]"
(at level 0, E, x at level 99,
format "[ '[hv' 'set' E '/ ' | x 'in' A & y 'in' B ] ']'").
Reserved Notation "[ 'set' 'of' F ]" (at level 0, format "[ 'set' 'of' F ]").
Reserved Notation "[ 'set' a ]"
(at level 0, a at level 99, format "[ 'set' a ]").
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 .`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 "\bigcup_ ( i 'in' P ) F"
(at level 41, F at level 41, i, P at level 50,
format "'[' \bigcup_ ( i 'in' P ) '/ ' F ']'").
Reserved Notation "\bigcup_ ( i : T ) F"
(at level 41, F at level 41, i at level 50,
format "'[' \bigcup_ ( i : T ) '/ ' F ']'").
Reserved Notation "\bigcup_ i F"
(at level 41, F at level 41, i at level 0,
format "'[' \bigcup_ i '/ ' F ']'").
Reserved Notation "\bigcap_ ( i 'in' P ) F"
(at level 41, F at level 41, i, P at level 50,
format "'[' \bigcap_ ( i 'in' P ) '/ ' F ']'").
Reserved Notation "\bigcap_ ( i : T ) F"
(at level 41, F at level 41, i at level 50,
format "'[' \bigcap_ ( i : T ) '/ ' F ']'").
Reserved Notation "\bigcap_ i F"
(at level 41, F at level 41, i at level 0,
format "'[' \bigcap_ i '/ ' F ']'").
Reserved Notation "A `<` B" (at level 70, no associativity).
Reserved Notation "A `<=` B" (at level 70, no associativity).
Reserved Notation "A `<=>` B" (at level 70, no associativity).
Reserved Notation "f @^-1` A" (at level 24).
Reserved Notation "f @` A" (at level 24).
Reserved Notation "A !=set0" (at level 80).
Reserved Notation "[ 'set`' p ]" (at level 0, format "[ 'set`' p ]").
Reserved Notation "[ 'disjoint' A & B ]" (at level 0,
format "'[hv' [ 'disjoint' '/ ' A '/' & B ] ']'").
Reserved Notation "f \|_ D" (at level 10).
Reserved Notation "F `#` G"
(at level 48, left associativity, format "F `#` G").
Definition gen_eq (T : Type) (u v : T) := `[<u = v>].
Lemma gen_eqP (T : Type) : Equality.axiom (@gen_eq T).
Definition gen_eqMixin {T : Type} := EqMixin (@gen_eqP T).
Canonical arrow_eqType (T : Type) (T' : eqType) :=
EqType (T → T') gen_eqMixin.
Canonical arrow_choiceType (T : Type) (T' : choiceType) :=
ChoiceType (T → T') gen_choiceMixin.
Definition dep_arrow_eqType (T : Type) (T' : T → eqType) :=
EqType (∀ x : T, T' x) gen_eqMixin.
Definition dep_arrow_choiceClass (T : Type) (T' : T → choiceType) :=
Choice.Class (Equality.class (dep_arrow_eqType T')) gen_choiceMixin.
Definition dep_arrow_choiceType (T : Type) (T' : T → choiceType) :=
Choice.Pack (dep_arrow_choiceClass T').
Canonical Prop_eqType := EqType Prop gen_eqMixin.
Canonical Prop_choiceType := ChoiceType Prop gen_choiceMixin.
Definition set T := T → Prop.
(at level 41, F at level 41, i, P at level 50,
format "'[' \bigcup_ ( i 'in' P ) '/ ' F ']'").
Reserved Notation "\bigcup_ ( i : T ) F"
(at level 41, F at level 41, i at level 50,
format "'[' \bigcup_ ( i : T ) '/ ' F ']'").
Reserved Notation "\bigcup_ i F"
(at level 41, F at level 41, i at level 0,
format "'[' \bigcup_ i '/ ' F ']'").
Reserved Notation "\bigcap_ ( i 'in' P ) F"
(at level 41, F at level 41, i, P at level 50,
format "'[' \bigcap_ ( i 'in' P ) '/ ' F ']'").
Reserved Notation "\bigcap_ ( i : T ) F"
(at level 41, F at level 41, i at level 50,
format "'[' \bigcap_ ( i : T ) '/ ' F ']'").
Reserved Notation "\bigcap_ i F"
(at level 41, F at level 41, i at level 0,
format "'[' \bigcap_ i '/ ' F ']'").
Reserved Notation "A `<` B" (at level 70, no associativity).
Reserved Notation "A `<=` B" (at level 70, no associativity).
Reserved Notation "A `<=>` B" (at level 70, no associativity).
Reserved Notation "f @^-1` A" (at level 24).
Reserved Notation "f @` A" (at level 24).
Reserved Notation "A !=set0" (at level 80).
Reserved Notation "[ 'set`' p ]" (at level 0, format "[ 'set`' p ]").
Reserved Notation "[ 'disjoint' A & B ]" (at level 0,
format "'[hv' [ 'disjoint' '/ ' A '/' & B ] ']'").
Reserved Notation "f \|_ D" (at level 10).
Reserved Notation "F `#` G"
(at level 48, left associativity, format "F `#` G").
Definition gen_eq (T : Type) (u v : T) := `[<u = v>].
Lemma gen_eqP (T : Type) : Equality.axiom (@gen_eq T).
Definition gen_eqMixin {T : Type} := EqMixin (@gen_eqP T).
Canonical arrow_eqType (T : Type) (T' : eqType) :=
EqType (T → T') gen_eqMixin.
Canonical arrow_choiceType (T : Type) (T' : choiceType) :=
ChoiceType (T → T') gen_choiceMixin.
Definition dep_arrow_eqType (T : Type) (T' : T → eqType) :=
EqType (∀ x : T, T' x) gen_eqMixin.
Definition dep_arrow_choiceClass (T : Type) (T' : T → choiceType) :=
Choice.Class (Equality.class (dep_arrow_eqType T')) gen_choiceMixin.
Definition dep_arrow_choiceType (T : Type) (T' : T → choiceType) :=
Choice.Pack (dep_arrow_choiceClass T').
Canonical Prop_eqType := EqType Prop gen_eqMixin.
Canonical Prop_choiceType := ChoiceType Prop gen_choiceMixin.
Definition set T := T → Prop.
we use fun x => instead of pred to prevent inE from working
we will then extend inE with in_setE to make this work
Definition in_set T (A : set T) : pred T := (fun x ⇒ `[<A x>]).
Canonical set_predType T := @PredType T (set T) (@in_set T).
Lemma in_setE T (A : set T) x : x \in A = A x :> Prop.
Definition inE := (inE, in_setE).
Bind Scope classical_set_scope with set.
Local Open Scope classical_set_scope.
Delimit Scope classical_set_scope with classic.
Definition mkset {T} (P : T → Prop) : set T := P.
Arguments mkset _ _ _ /.
Notation "[ 'set' x : T | P ]" := (mkset (fun x : T ⇒ P)) : classical_set_scope.
Notation "[ 'set' x | P ]" := [set x : _ | P] : classical_set_scope.
Definition image {T rT} (A : set T) (f : T → rT) :=
[set y | exists2 x, A x & f x = y].
Arguments image _ _ _ _ _ /.
Notation "[ 'set' E | x 'in' A ]" :=
(image A (fun x ⇒ E)) : classical_set_scope.
Definition image2 {TA TB rT} (A : set TA) (B : set TB) (f : TA → TB → rT) :=
[set z | exists2 x, A x & exists2 y, B y & f x y = z].
Arguments image2 _ _ _ _ _ _ _ /.
Notation "[ 'set' E | x 'in' A & y 'in' B ]" :=
(image2 A B (fun x y ⇒ E)) : classical_set_scope.
Section basic_definitions.
Context {T rT : Type}.
Implicit Types (T : Type) (A B : set T) (f : T → rT) (Y : set rT).
Definition preimage f Y : set T := [set t | Y (f t)].
Definition setT := [set _ : T | True].
Definition set0 := [set _ : T | False].
Definition set1 (t : T) := [set x : T | x = t].
Definition setI A B := [set x | A x ∧ B x].
Definition setU A B := [set x | A x ∨ B x].
Definition nonempty A := ∃ a, A a.
Definition setC A := [set a | ¬ A a].
Definition setD A B := [set x | A x ∧ ¬ B x].
Definition setM T1 T2 (A1 : set T1) (A2 : set T2) := [set z | A1 z.1 ∧ A2 z.2].
Definition fst_set T1 T2 (A : set (T1 × T2)) := [set x | ∃ y, A (x, y)].
Definition snd_set T1 T2 (A : set (T1 × T2)) := [set y | ∃ x, A (x, y)].
Lemma mksetE (P : T → Prop) x : [set x | P x] x = P x.
Definition bigcap T I (P : set I) (F : I → set T) :=
[set a | ∀ i, P i → F i a].
Definition bigcup T I (P : set I) (F : I → set T) :=
[set a | exists2 i, P i & F i a].
Definition subset A B := ∀ t, A t → B t.
Definition 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 fst_set _ _ _ _ /.
Arguments snd_set _ _ _ _ /.
Notation "[ 'set' 'of' F ]" := [set F i | i in setT] : classical_set_scope.
Notation "[ 'set' a ]" := (set1 a) : classical_set_scope.
Notation "[ 'set' a : T ]" := [set (a : 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" := (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 ]" := (A `&` B == set0) : classical_set_scope.
Notation "\bigcup_ ( i 'in' P ) F" :=
(bigcup P (fun i ⇒ F)) : classical_set_scope.
Notation "\bigcup_ ( i : T ) F" :=
(\bigcup_(i in @setT T) F) : classical_set_scope.
Notation "\bigcup_ i F" := (\bigcup_(i : _) F) : classical_set_scope.
Notation "\bigcap_ ( i 'in' P ) F" :=
(bigcap P (fun i ⇒ F)) : classical_set_scope.
Notation "\bigcap_ ( i : T ) F" :=
(\bigcap_(i in @setT T) F) : classical_set_scope.
Notation "\bigcap_ i F" := (\bigcap_(i : _) F) : classical_set_scope.
Notation "A `<=` B" := (subset A B) : classical_set_scope.
Notation "A `<` B" := (proper A B) : classical_set_scope.
Notation "A `<=>` B" := ((A `<=` B) ∧ (B `<=` A)) : classical_set_scope.
Notation "f @^-1` A" := (preimage f A) : classical_set_scope.
Notation "f @` A" := (image A f) (only parsing) : classical_set_scope.
Notation "A !=set0" := (nonempty A) : classical_set_scope.
Notation "[ 'set`' p ]":= [set x | is_true (x \in p)] : classical_set_scope.
Notation pred_set := (fun i ⇒ [set` i]).
Notation "`[ a , b ]" :=
[set` Interval (BLeft a) (BRight b)] : classical_set_scope.
Notation "`] a , b ]" :=
[set` Interval (BRight a) (BRight b)] : classical_set_scope.
Notation "`[ a , b [" :=
[set` Interval (BLeft a) (BLeft b)] : classical_set_scope.
Notation "`] a , b [" :=
[set` Interval (BRight a) (BLeft b)] : classical_set_scope.
Notation "`] '-oo' , b ]" :=
[set` Interval -oo%O (BRight b)] : classical_set_scope.
Notation "`] '-oo' , b [" :=
[set` Interval -oo%O (BLeft b)] : classical_set_scope.
Notation "`[ a , '+oo' [" :=
[set` Interval (BLeft a) +oo%O] : classical_set_scope.
Notation "`] a , '+oo' [" :=
[set` Interval (BRight a) +oo%O] : classical_set_scope.
Notation "`] -oo , '+oo' [" :=
[set` Interval -oo%O +oo%O] : classical_set_scope.
Lemma eq_set T (P Q : T → Prop) : (∀ x : T, P x = Q x) →
[set x | P x] = [set x | Q x].
Section basic_lemmas.
Context {T : Type}.
Implicit Types A B C D : set T.
Lemma eqEsubset A B : (A = B) = (A `<=>` B).
Lemma seteqP A B : (A = B) ↔ (A `<=>` B).
Lemma subset_trans B A C : A `<=` B → B `<=` C → A `<=` C.
Lemma sub0set A : set0 `<=` A.
Lemma setC0 : ~` set0 = setT :> set T.
Lemma setCK : involutive (@setC T).
Definition setC_inj := can_inj setCK.
Lemma setIC : commutative (@setI T).
Lemma setIS C A B : A `<=` B → C `&` A `<=` C `&` B.
Lemma setSI C A B : A `<=` B → A `&` C `<=` B `&` C.
Lemma setISS A B C D : A `<=` C → B `<=` D → A `&` B `<=` C `&` D.
Lemma setIT : right_id setT (@setI T).
Lemma setTI : left_id setT (@setI T).
Lemma setI0 : right_zero set0 (@setI T).
Lemma set0I : left_zero set0 (@setI T).
Lemma setICl : left_inverse set0 setC (@setI T).
Lemma setICr : right_inverse set0 setC (@setI T).
Lemma setIA : associative (@setI T).
Lemma setICA : left_commutative (@setI T).
Lemma setIAC : right_commutative (@setI T).
Lemma setIACA : @interchange (set T) setI setI.
Lemma setIid : idempotent (@setI T).
Lemma setIIl A B C : A `&` B `&` C = (A `&` C) `&` (B `&` C).
Lemma setIIr A B C : A `&` (B `&` C) = (A `&` B) `&` (A `&` C).
Lemma setUC : commutative (@setU T).
Lemma setUS C A B : A `<=` B → C `|` A `<=` C `|` B.
Lemma setSU C A B : A `<=` B → A `|` C `<=` B `|` C.
Lemma setUSS A B C D : A `<=` C → B `<=` D → A `|` B `<=` C `|` D.
Lemma setTU : left_zero setT (@setU T).
Lemma setUT : right_zero setT (@setU T).
Lemma set0U : left_id set0 (@setU T).
Lemma setU0 : right_id set0 (@setU T).
Lemma setUCl : left_inverse setT setC (@setU T).
Lemma setUCr : right_inverse setT setC (@setU T).
Lemma setUA : associative (@setU T).
Lemma setUCA : left_commutative (@setU T).
Lemma setUAC : right_commutative (@setU T).
Lemma setUACA : @interchange (set T) setU setU.
Lemma setUid : idempotent (@setU T).
Lemma setUUl A B C : A `|` B `|` C = (A `|` C) `|` (B `|` C).
Lemma setUUr A B C : A `|` (B `|` C) = (A `|` B) `|` (A `|` C).
Lemma setD1K a A : A a → a |` A `\ a = A.
Lemma subsets_disjoint A B : (A `<=` B) ↔ (A `&` ~` B = set0).
Lemma disjoints_subset A B : A `&` B = set0 ↔ A `<=` ~` B.
Lemma setCT : ~` setT = set0 :> set T.
Lemma subsetC1 x A : (A `<=` [set¬ x]) = (x \in ~` A).
Lemma setDE A B : A `\` B = A `&` ~` B.
Lemma setSD C A B : A `<=` B → A `\` C `<=` B `\` C.
Lemma setTD A : setT `\` A = ~` A.
Lemma setDv A : A `\` A = set0.
Lemma subset0 A : (A `<=` set0) = (A = set0).
Lemma subTset A : (setT `<=` A) = (A = setT).
Lemma set0P A : (A != set0) ↔ (A !=set0).
Lemma subset_nonempty A B : A `<=` B → A !=set0 → B !=set0.
Lemma subsetC A B : A `<=` B → ~` B `<=` ~` A.
Lemma subsetU A B C : A `<=` C → B `<=` C → A `|` B `<=` C.
Lemma subUset A B C : (B `|` C `<=` A) = ((B `<=` A) ∧ (C `<=` A)).
Lemma setIidPl A B : A `&` B = A ↔ A `<=` B.
Lemma setIidPr A B : A `&` B = B ↔ B `<=` A.
Lemma setIidl A B : A `<=` B → A `&` B = A.
Lemma setIidr A B : B `<=` A → A `&` B = B.
Lemma setUidPl A B : A `|` B = A ↔ B `<=` A.
Lemma setUidPr A B : A `|` B = B ↔ A `<=` B.
Lemma setUidl A B : B `<=` A → A `|` B = A.
Lemma setUidr A B : A `<=` B → A `|` B = B.
Lemma subsetI A B C : (A `<=` B `&` C) = ((A `<=` B) ∧ (A `<=` C)).
Lemma setDidPl A B : A `\` B = A ↔ A `&` B = set0.
Lemma subIset A B C : A `<=` C ∨ B `<=` C → A `&` B `<=` C.
Lemma subsetI_neq0 A B C D :
A `<=` B → C `<=` D → A `&` C !=set0 → B `&` D !=set0.
Lemma subsetI_eq0 A B C D :
A `<=` B → C `<=` D → B `&` D = set0 → A `&` C = set0.
Lemma setD_eq0 A B : (A `\` B = set0) = (A `<=` B).
Lemma properEneq A B : (A `<` B) = (A != B ∧ A `<=` B).
Lemma nonsubset A B : ¬ (A `<=` B) → A `&` ~` B !=set0.
Lemma setU_eq0 A B : (A `|` B = set0) = ((A = set0) ∧ (B = set0)).
Lemma setCS A B : (~` A `<=` ~` B) = (B `<=` A).
Lemma setDT A : A `\` setT = set0.
Lemma set0D A : set0 `\` A = set0.
Lemma setD0 A : A `\` set0 = A.
Lemma setDS C A B : A `<=` B → C `\` B `<=` C `\` A.
Lemma setDSS A B C D : A `<=` C → D `<=` B → A `\` B `<=` C `\` D.
Lemma setCU A B : ~`(A `|` B) = ~` A `&` ~` B.
Lemma setCI A B : ~` (A `&` B) = ~` A `|` ~` B.
Lemma setDUr A B C : A `\` (B `|` C) = (A `\` B) `&` (A `\` C).
Lemma setIUl : left_distributive (@setI T) (@setU T).
Lemma setIUr : right_distributive (@setI T) (@setU T).
Lemma setUIl : left_distributive (@setU T) (@setI T).
Lemma setUIr : right_distributive (@setU T) (@setI T).
Lemma setUK A B : (A `|` B) `&` A = A.
Lemma setKU A B : A `&` (B `|` A) = A.
Lemma setIK A B : (A `&` B) `|` A = A.
Lemma setKI A B : A `|` (B `&` A) = A.
Lemma setDUl : left_distributive setD (@setU T).
Lemma setIDA A B C : A `&` (B `\` C) = (A `&` B) `\` C.
Lemma setDD A B : A `\` (A `\` B) = A `&` B.
Lemma setDDl A B C : (A `\` B) `\` C = A `\` (B `|` C).
Lemma setDDr A B C : A `\` (B `\` C) = (A `\` B) `|` (A `&` C).
Lemma setDIr A B C : A `\` B `&` C = (A `\` B) `|` (A `\` C).
Lemma setM0 T' (A : set T) : A `*` set0 = set0 :> set (T × T').
Lemma set0M T' (A : set T') : set0 `*` A = set0 :> set (T × T').
Lemma setMTT T' : setT `*` setT = setT :> set (T × T').
Lemma setMT T1 T2 (A : set T1) : A `*` @setT T2 = fst @^-1` A.
Lemma setTM T1 T2 (B : set T2) : @setT T1 `*` B = snd @^-1` B.
Lemma setMI T1 T2 (X1 : set T1) (X2 : set T2) (Y1 : set T1) (Y2 : set T2) :
(X1 `&` Y1) `*` (X2 `&` Y2) = X1 `*` X2 `&` Y1 `*` Y2.
Lemma setSM T1 T2 (C D : set T1) (A B : set T2) :
A `<=` B → C `<=` D → C `*` A `<=` D `*` B.
Lemma setM_bigcupr T1 T2 I (F : I → set T2) (P : set I) (A : set T1) :
A `*` \bigcup_(i in P) F i = \bigcup_(i in P) (A `*` F i).
Lemma setM_bigcupl T1 T2 I (F : I → set T2) (P : set I) (A : set T1) :
\bigcup_(i in P) F i `*` A = \bigcup_(i in P) (F i `*` A).
Lemma notin_set (A : set T) x : (x \notin A : Prop) = ¬ (A x).
End basic_lemmas.
Lemma mkset_nil (T : choiceType) : [set x | x \in [::]] = @set0 T.
Canonical set_predType T := @PredType T (set T) (@in_set T).
Lemma in_setE T (A : set T) x : x \in A = A x :> Prop.
Definition inE := (inE, in_setE).
Bind Scope classical_set_scope with set.
Local Open Scope classical_set_scope.
Delimit Scope classical_set_scope with classic.
Definition mkset {T} (P : T → Prop) : set T := P.
Arguments mkset _ _ _ /.
Notation "[ 'set' x : T | P ]" := (mkset (fun x : T ⇒ P)) : classical_set_scope.
Notation "[ 'set' x | P ]" := [set x : _ | P] : classical_set_scope.
Definition image {T rT} (A : set T) (f : T → rT) :=
[set y | exists2 x, A x & f x = y].
Arguments image _ _ _ _ _ /.
Notation "[ 'set' E | x 'in' A ]" :=
(image A (fun x ⇒ E)) : classical_set_scope.
Definition image2 {TA TB rT} (A : set TA) (B : set TB) (f : TA → TB → rT) :=
[set z | exists2 x, A x & exists2 y, B y & f x y = z].
Arguments image2 _ _ _ _ _ _ _ /.
Notation "[ 'set' E | x 'in' A & y 'in' B ]" :=
(image2 A B (fun x y ⇒ E)) : classical_set_scope.
Section basic_definitions.
Context {T rT : Type}.
Implicit Types (T : Type) (A B : set T) (f : T → rT) (Y : set rT).
Definition preimage f Y : set T := [set t | Y (f t)].
Definition setT := [set _ : T | True].
Definition set0 := [set _ : T | False].
Definition set1 (t : T) := [set x : T | x = t].
Definition setI A B := [set x | A x ∧ B x].
Definition setU A B := [set x | A x ∨ B x].
Definition nonempty A := ∃ a, A a.
Definition setC A := [set a | ¬ A a].
Definition setD A B := [set x | A x ∧ ¬ B x].
Definition setM T1 T2 (A1 : set T1) (A2 : set T2) := [set z | A1 z.1 ∧ A2 z.2].
Definition fst_set T1 T2 (A : set (T1 × T2)) := [set x | ∃ y, A (x, y)].
Definition snd_set T1 T2 (A : set (T1 × T2)) := [set y | ∃ x, A (x, y)].
Lemma mksetE (P : T → Prop) x : [set x | P x] x = P x.
Definition bigcap T I (P : set I) (F : I → set T) :=
[set a | ∀ i, P i → F i a].
Definition bigcup T I (P : set I) (F : I → set T) :=
[set a | exists2 i, P i & F i a].
Definition subset A B := ∀ t, A t → B t.
Definition 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 fst_set _ _ _ _ /.
Arguments snd_set _ _ _ _ /.
Notation "[ 'set' 'of' F ]" := [set F i | i in setT] : classical_set_scope.
Notation "[ 'set' a ]" := (set1 a) : classical_set_scope.
Notation "[ 'set' a : T ]" := [set (a : 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" := (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 ]" := (A `&` B == set0) : classical_set_scope.
Notation "\bigcup_ ( i 'in' P ) F" :=
(bigcup P (fun i ⇒ F)) : classical_set_scope.
Notation "\bigcup_ ( i : T ) F" :=
(\bigcup_(i in @setT T) F) : classical_set_scope.
Notation "\bigcup_ i F" := (\bigcup_(i : _) F) : classical_set_scope.
Notation "\bigcap_ ( i 'in' P ) F" :=
(bigcap P (fun i ⇒ F)) : classical_set_scope.
Notation "\bigcap_ ( i : T ) F" :=
(\bigcap_(i in @setT T) F) : classical_set_scope.
Notation "\bigcap_ i F" := (\bigcap_(i : _) F) : classical_set_scope.
Notation "A `<=` B" := (subset A B) : classical_set_scope.
Notation "A `<` B" := (proper A B) : classical_set_scope.
Notation "A `<=>` B" := ((A `<=` B) ∧ (B `<=` A)) : classical_set_scope.
Notation "f @^-1` A" := (preimage f A) : classical_set_scope.
Notation "f @` A" := (image A f) (only parsing) : classical_set_scope.
Notation "A !=set0" := (nonempty A) : classical_set_scope.
Notation "[ 'set`' p ]":= [set x | is_true (x \in p)] : classical_set_scope.
Notation pred_set := (fun i ⇒ [set` i]).
Notation "`[ a , b ]" :=
[set` Interval (BLeft a) (BRight b)] : classical_set_scope.
Notation "`] a , b ]" :=
[set` Interval (BRight a) (BRight b)] : classical_set_scope.
Notation "`[ a , b [" :=
[set` Interval (BLeft a) (BLeft b)] : classical_set_scope.
Notation "`] a , b [" :=
[set` Interval (BRight a) (BLeft b)] : classical_set_scope.
Notation "`] '-oo' , b ]" :=
[set` Interval -oo%O (BRight b)] : classical_set_scope.
Notation "`] '-oo' , b [" :=
[set` Interval -oo%O (BLeft b)] : classical_set_scope.
Notation "`[ a , '+oo' [" :=
[set` Interval (BLeft a) +oo%O] : classical_set_scope.
Notation "`] a , '+oo' [" :=
[set` Interval (BRight a) +oo%O] : classical_set_scope.
Notation "`] -oo , '+oo' [" :=
[set` Interval -oo%O +oo%O] : classical_set_scope.
Lemma eq_set T (P Q : T → Prop) : (∀ x : T, P x = Q x) →
[set x | P x] = [set x | Q x].
Section basic_lemmas.
Context {T : Type}.
Implicit Types A B C D : set T.
Lemma eqEsubset A B : (A = B) = (A `<=>` B).
Lemma seteqP A B : (A = B) ↔ (A `<=>` B).
Lemma subset_trans B A C : A `<=` B → B `<=` C → A `<=` C.
Lemma sub0set A : set0 `<=` A.
Lemma setC0 : ~` set0 = setT :> set T.
Lemma setCK : involutive (@setC T).
Definition setC_inj := can_inj setCK.
Lemma setIC : commutative (@setI T).
Lemma setIS C A B : A `<=` B → C `&` A `<=` C `&` B.
Lemma setSI C A B : A `<=` B → A `&` C `<=` B `&` C.
Lemma setISS A B C D : A `<=` C → B `<=` D → A `&` B `<=` C `&` D.
Lemma setIT : right_id setT (@setI T).
Lemma setTI : left_id setT (@setI T).
Lemma setI0 : right_zero set0 (@setI T).
Lemma set0I : left_zero set0 (@setI T).
Lemma setICl : left_inverse set0 setC (@setI T).
Lemma setICr : right_inverse set0 setC (@setI T).
Lemma setIA : associative (@setI T).
Lemma setICA : left_commutative (@setI T).
Lemma setIAC : right_commutative (@setI T).
Lemma setIACA : @interchange (set T) setI setI.
Lemma setIid : idempotent (@setI T).
Lemma setIIl A B C : A `&` B `&` C = (A `&` C) `&` (B `&` C).
Lemma setIIr A B C : A `&` (B `&` C) = (A `&` B) `&` (A `&` C).
Lemma setUC : commutative (@setU T).
Lemma setUS C A B : A `<=` B → C `|` A `<=` C `|` B.
Lemma setSU C A B : A `<=` B → A `|` C `<=` B `|` C.
Lemma setUSS A B C D : A `<=` C → B `<=` D → A `|` B `<=` C `|` D.
Lemma setTU : left_zero setT (@setU T).
Lemma setUT : right_zero setT (@setU T).
Lemma set0U : left_id set0 (@setU T).
Lemma setU0 : right_id set0 (@setU T).
Lemma setUCl : left_inverse setT setC (@setU T).
Lemma setUCr : right_inverse setT setC (@setU T).
Lemma setUA : associative (@setU T).
Lemma setUCA : left_commutative (@setU T).
Lemma setUAC : right_commutative (@setU T).
Lemma setUACA : @interchange (set T) setU setU.
Lemma setUid : idempotent (@setU T).
Lemma setUUl A B C : A `|` B `|` C = (A `|` C) `|` (B `|` C).
Lemma setUUr A B C : A `|` (B `|` C) = (A `|` B) `|` (A `|` C).
Lemma setD1K a A : A a → a |` A `\ a = A.
Lemma subsets_disjoint A B : (A `<=` B) ↔ (A `&` ~` B = set0).
Lemma disjoints_subset A B : A `&` B = set0 ↔ A `<=` ~` B.
Lemma setCT : ~` setT = set0 :> set T.
Lemma subsetC1 x A : (A `<=` [set¬ x]) = (x \in ~` A).
Lemma setDE A B : A `\` B = A `&` ~` B.
Lemma setSD C A B : A `<=` B → A `\` C `<=` B `\` C.
Lemma setTD A : setT `\` A = ~` A.
Lemma setDv A : A `\` A = set0.
Lemma subset0 A : (A `<=` set0) = (A = set0).
Lemma subTset A : (setT `<=` A) = (A = setT).
Lemma set0P A : (A != set0) ↔ (A !=set0).
Lemma subset_nonempty A B : A `<=` B → A !=set0 → B !=set0.
Lemma subsetC A B : A `<=` B → ~` B `<=` ~` A.
Lemma subsetU A B C : A `<=` C → B `<=` C → A `|` B `<=` C.
Lemma subUset A B C : (B `|` C `<=` A) = ((B `<=` A) ∧ (C `<=` A)).
Lemma setIidPl A B : A `&` B = A ↔ A `<=` B.
Lemma setIidPr A B : A `&` B = B ↔ B `<=` A.
Lemma setIidl A B : A `<=` B → A `&` B = A.
Lemma setIidr A B : B `<=` A → A `&` B = B.
Lemma setUidPl A B : A `|` B = A ↔ B `<=` A.
Lemma setUidPr A B : A `|` B = B ↔ A `<=` B.
Lemma setUidl A B : B `<=` A → A `|` B = A.
Lemma setUidr A B : A `<=` B → A `|` B = B.
Lemma subsetI A B C : (A `<=` B `&` C) = ((A `<=` B) ∧ (A `<=` C)).
Lemma setDidPl A B : A `\` B = A ↔ A `&` B = set0.
Lemma subIset A B C : A `<=` C ∨ B `<=` C → A `&` B `<=` C.
Lemma subsetI_neq0 A B C D :
A `<=` B → C `<=` D → A `&` C !=set0 → B `&` D !=set0.
Lemma subsetI_eq0 A B C D :
A `<=` B → C `<=` D → B `&` D = set0 → A `&` C = set0.
Lemma setD_eq0 A B : (A `\` B = set0) = (A `<=` B).
Lemma properEneq A B : (A `<` B) = (A != B ∧ A `<=` B).
Lemma nonsubset A B : ¬ (A `<=` B) → A `&` ~` B !=set0.
Lemma setU_eq0 A B : (A `|` B = set0) = ((A = set0) ∧ (B = set0)).
Lemma setCS A B : (~` A `<=` ~` B) = (B `<=` A).
Lemma setDT A : A `\` setT = set0.
Lemma set0D A : set0 `\` A = set0.
Lemma setD0 A : A `\` set0 = A.
Lemma setDS C A B : A `<=` B → C `\` B `<=` C `\` A.
Lemma setDSS A B C D : A `<=` C → D `<=` B → A `\` B `<=` C `\` D.
Lemma setCU A B : ~`(A `|` B) = ~` A `&` ~` B.
Lemma setCI A B : ~` (A `&` B) = ~` A `|` ~` B.
Lemma setDUr A B C : A `\` (B `|` C) = (A `\` B) `&` (A `\` C).
Lemma setIUl : left_distributive (@setI T) (@setU T).
Lemma setIUr : right_distributive (@setI T) (@setU T).
Lemma setUIl : left_distributive (@setU T) (@setI T).
Lemma setUIr : right_distributive (@setU T) (@setI T).
Lemma setUK A B : (A `|` B) `&` A = A.
Lemma setKU A B : A `&` (B `|` A) = A.
Lemma setIK A B : (A `&` B) `|` A = A.
Lemma setKI A B : A `|` (B `&` A) = A.
Lemma setDUl : left_distributive setD (@setU T).
Lemma setIDA A B C : A `&` (B `\` C) = (A `&` B) `\` C.
Lemma setDD A B : A `\` (A `\` B) = A `&` B.
Lemma setDDl A B C : (A `\` B) `\` C = A `\` (B `|` C).
Lemma setDDr A B C : A `\` (B `\` C) = (A `\` B) `|` (A `&` C).
Lemma setDIr A B C : A `\` B `&` C = (A `\` B) `|` (A `\` C).
Lemma setM0 T' (A : set T) : A `*` set0 = set0 :> set (T × T').
Lemma set0M T' (A : set T') : set0 `*` A = set0 :> set (T × T').
Lemma setMTT T' : setT `*` setT = setT :> set (T × T').
Lemma setMT T1 T2 (A : set T1) : A `*` @setT T2 = fst @^-1` A.
Lemma setTM T1 T2 (B : set T2) : @setT T1 `*` B = snd @^-1` B.
Lemma setMI T1 T2 (X1 : set T1) (X2 : set T2) (Y1 : set T1) (Y2 : set T2) :
(X1 `&` Y1) `*` (X2 `&` Y2) = X1 `*` X2 `&` Y1 `*` Y2.
Lemma setSM T1 T2 (C D : set T1) (A B : set T2) :
A `<=` B → C `<=` D → C `*` A `<=` D `*` B.
Lemma setM_bigcupr T1 T2 I (F : I → set T2) (P : set I) (A : set T1) :
A `*` \bigcup_(i in P) F i = \bigcup_(i in P) (A `*` F i).
Lemma setM_bigcupl T1 T2 I (F : I → set T2) (P : set I) (A : set T1) :
\bigcup_(i in P) F i `*` A = \bigcup_(i in P) (F i `*` A).
Lemma notin_set (A : set T) x : (x \notin A : Prop) = ¬ (A x).
End basic_lemmas.
Lemma mkset_nil (T : choiceType) : [set x | x \in [::]] = @set0 T.
TODO: other lemmas that relate fset and classical sets
Lemma fdisjoint_cset (T : choiceType) (A B : {fset T}) :
[disjoint A & B]%fset = [disjoint [set x | x \in A] & [set x | x \in B]].
Section SetFset.
Context {T : choiceType}.
Implicit Types (x y : T) (A B : {fset T}).
Lemma set_fset0 : [set y : T | y \in fset0] = set0.
Lemma set_fset1 x : [set y | y \in [fset x]%fset] = [set x].
Lemma set_fsetI A B :
[set x | x \in (A `&` B)%fset] = [set x | x \in A] `&` [set x | x \in B].
Lemma set_fsetU A B :
[set x | x \in (A `|` B)%fset] = [set x | x \in A] `|` [set x | x \in B].
Lemma set_fsetU1 x A : [set y | y \in (x |` A)%fset] = x |` [set x | x \in A].
Lemma set_fsetD A B :
[set x | x \in (A `\` B)%fset] = [set x | x \in A] `\` [set x | x \in B].
Lemma set_fsetD1 A x : [set y | y \in (A `\ x)%fset] = [set x | x \in A] `\ x.
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 image_lemmas.
Context {aT rT : Type}.
Implicit Types (A B : set aT) (f : aT → rT) (Y : set rT).
Lemma imageP f A a : A a → (f @` A) (f a).
Lemma image_inj {f A a} : injective f → (f @` A) (f a) = A a.
Lemma image_id A : id @` A = A.
Lemma image_setU f A B : f @` (A `|` B) = f @` A `|` f @` B.
Lemma image_set0 f : f @` set0 = set0.
Lemma image_set0_set0 A f : f @` A = set0 → A = set0.
Lemma image_set1 f t : f @` [set t] = [set f t].
Lemma subset_set1 A a : A `<=` [set a] → A = set0 ∨ A = [set a].
Lemma sub_image_setI f A B : f @` (A `&` B) `<=` f @` A `&` f @` B.
Lemma nonempty_image f A : f @` A !=set0 → A !=set0.
Lemma image_subset f A B : A `<=` B → f @` A `<=` f @` B.
Lemma preimage_set0 f : f @^-1` set0 = set0.
Lemma nonempty_preimage f Y : f @^-1` Y !=set0 → Y !=set0.
Lemma preimage_image f A : A `<=` f @^-1` (f @` A).
Lemma image_preimage_subset f Y : f @` (f @^-1` Y) `<=` Y.
Lemma image_preimage f Y : f @` setT = setT → f @` (f @^-1` Y) = Y.
Lemma eq_imagel T1 T2 (A : set T1) (f f' : T1 → T2) :
(∀ x, A x → f x = f' x) → f @` A = f' @` A.
Lemma preimage_setU f Y1 Y2 : f @^-1` (Y1 `|` Y2) = f @^-1` Y1 `|` f @^-1` Y2.
Lemma preimage_setI f Y1 Y2 : f @^-1` (Y1 `&` Y2) = f @^-1` Y1 `&` f @^-1` Y2.
Lemma preimage_setC f Y : ~` (f @^-1` Y) = f @^-1` (~` Y).
Lemma preimage_subset f Y1 Y2 : Y1 `<=` Y2 → f @^-1` Y1 `<=` f @^-1` Y2.
Lemma nonempty_preimage_setI f Y1 Y2 :
(f @^-1` (Y1 `&` Y2)) !=set0 ↔ (f @^-1` Y1 `&` f @^-1` Y2) !=set0.
Lemma preimage_bigcup {I} (P : set I) f (F : I → set rT) :
f @^-1` (\bigcup_ (i in P) F i) = \bigcup_(i in P) (f @^-1` F i).
Lemma preimage_bigcap {I} (P : set I) f (F : I → set rT) :
f @^-1` (\bigcap_ (i in P) F i) = \bigcap_(i in P) (f @^-1` F i).
End image_lemmas.
Arguments sub_image_setI {aT rT f A B} t _.
Lemma image_comp T1 T2 T3 (f : T1 → T2) (g : T2 → T3) A :
g @` (f @` A) = (g \o f) @` A.
Section bigop_lemmas.
Context {T I : Type}.
Implicit Types (A : set T) (i : I) (P : set I) (F G : I → set T).
Lemma bigcup_sup i P F : P i → F i `<=` \bigcup_(j in P) F j.
Lemma bigcap_inf i P F : P i → \bigcap_(j in P) F j `<=` F i.
Lemma subset_bigcup_r P : {homo (fun x : I → set T ⇒ \bigcup_(i in P) x i)
: F G / [set F i | i in P] `<=` [set G i | i in P] >-> F `<=` G}.
Lemma subset_bigcap_r P : {homo (fun x : I → set T ⇒ \bigcap_(i in P) x i)
: F G / [set F i | i in P] `<=` [set G i | i in P] >-> G `<=` F}.
Lemma eq_bigcupr P F G : (∀ i, P i → F i = G i) →
\bigcup_(i in P) F i = \bigcup_(i in P) G i.
Lemma eq_bigcapr P F G : (∀ i, P i → F i = G i) →
\bigcap_(i in P) F i = \bigcap_(i in P) G i.
Lemma setC_bigcup P F : ~` (\bigcup_(i in P) F i) = \bigcap_(i in P) ~` F i.
Lemma setC_bigcap P F : ~` (\bigcap_(i in P) (F i)) = \bigcup_(i in P) ~` F i.
Lemma eq_bigcupl P Q F : P `<=>` Q →
\bigcup_(i in P) F i = \bigcup_(i in Q) F i.
Lemma eq_bigcapl P Q F : P `<=>` Q →
\bigcap_(i in P) F i = \bigcap_(i in Q) F i.
Lemma eq_bigcup P Q F G : P `<=>` Q → (∀ i, P i → F i = G i) →
\bigcup_(i in P) F i = \bigcup_(i in Q) G i.
Lemma eq_bigcap P Q F G : P `<=>` Q → (∀ i, P i → F i = G i) →
\bigcap_(i in P) F i = \bigcap_(i in Q) G i.
Lemma bigcupU P F G : \bigcup_(i in P) (F i `|` G i) =
(\bigcup_(i in P) F i) `|` (\bigcup_(i in P) G i).
Lemma bigcapI P F G : \bigcap_(i in P) (F i `&` G i) =
(\bigcap_(i in P) F i) `&` (\bigcap_(i in P) G i).
Lemma bigcup_const P A : P !=set0 → \bigcup_(_ in P) A = A.
Lemma bigcap_const P A : P !=set0 → \bigcap_(_ in P) A = A.
Lemma bigcapIl P F A : P !=set0 →
\bigcap_(i in P) (F i `&` A) = \bigcap_(i in P) F i `&` A.
Lemma bigcapIr P F A : P !=set0 →
\bigcap_(i in P) (A `&` F i) = A `&` \bigcap_(i in P) F i.
Lemma bigcupUl P F A : P !=set0 →
\bigcup_(i in P) (F i `|` A) = \bigcup_(i in P) F i `|` A.
Lemma bigcupUr P F A : P !=set0 →
\bigcup_(i in P) (A `|` F i) = A `|` \bigcup_(i in P) F i.
Lemma bigcup_set0 F : \bigcup_(i in set0) F i = set0.
Lemma bigcup_set1 F i : \bigcup_(j in [set i]) F j = F i.
Lemma bigcap_set0 F : \bigcap_(i in set0) F i = setT.
Lemma bigcap_set1 F i : \bigcap_(j in [set i]) F j = F i.
Lemma bigcup_nonempty P F :
(\bigcup_(i in P) F i !=set0) ↔ exists2 i, P i & F i !=set0.
Lemma bigcup0 P F :
(∀ i, P i → F i = set0) → \bigcup_(i in P) F i = set0.
Lemma bigcap0 P F :
(exists2 i, P i & F i = set0) → \bigcap_(i in P) F i = set0.
Lemma bigcapT P F :
(∀ i, P i → F i = setT) → \bigcap_(i in P) F i = setT.
Lemma bigcupT P F :
(exists2 i, P i & F i = setT) → \bigcup_(i in P) F i = setT.
Lemma bigcup0P P F :
(\bigcup_(i in P) F i = set0) ↔ ∀ i, P i → F i = set0.
Lemma bigcapTP P F :
(\bigcap_(i in P) F i = setT) ↔ ∀ i, P i → F i = setT.
Lemma setI_bigcupr F P A :
A `&` \bigcup_(i in P) F i = \bigcup_(i in P) (A `&` F i).
Lemma setI_bigcupl F P A :
\bigcup_(i in P) F i `&` A = \bigcup_(i in P) (F i `&` A).
Lemma setU_bigcapr F P A :
A `|` \bigcap_(i in P) F i = \bigcap_(i in P) (A `|` F i).
Lemma setU_bigcapl F P A :
\bigcap_(i in P) F i `|` A = \bigcap_(i in P) (F i `|` A).
Lemma bigcup_mkcond F P :
\bigcup_(i in P) F i = \bigcup_i if `[< P i >] then F i else set0.
Lemma bigcap_mkcond F P :
\bigcap_(i in P) F i = \bigcap_i if `[< P i >] then F i else setT.
Lemma bigcup_imset1 P (f : I → T) : \bigcup_(x in P) [set f x] = f @` P.
Lemma bigcup_setU F (X Y : set I) :
\bigcup_(i in X `|` Y) F i = \bigcup_(i in X) F i `|` \bigcup_(i in Y) F i.
Lemma bigcap_setU F (X Y : set I) :
\bigcap_(i in X `|` Y) F i = \bigcap_(i in X) F i `&` \bigcap_(i in Y) F i.
Lemma bigcup_setU1 F (x : I) (X : set I) :
\bigcup_(i in x |` X) F i = F x `|` \bigcup_(i in X) F i.
Lemma bigcap_setU1 F (x : I) (X : set I) :
\bigcap_(i in x |` X) F i = F x `&` \bigcap_(i in X) F i.
Lemma bigcup_setD1 (x : I) F (X : set I) : X x →
\bigcup_(i in X) F i = F x `|` \bigcup_(i in X `\ x) F i.
Lemma bigcap_setD1 (x : I) F (X : set I) : X x →
\bigcap_(i in X) F i = F x `&` \bigcap_(i in X `\ x) F i.
Lemma setC_bigsetU U (s : seq T) (f : T → set U) (P : pred T) :
(~` \big[setU/set0]_(t <- s | P t) f t) = \big[setI/setT]_(t <- s | P t) ~` f t.
Lemma setC_bigsetI U (s : seq T) (f : T → set U) (P : pred T) :
(~` \big[setI/setT]_(t <- s | P t) f t) = \big[setU/set0]_(t <- s | P t) ~` f t.
End bigop_lemmas.
Arguments bigcup_setD1 {T I} x.
Arguments bigcap_setD1 {T I} x.
Lemma bigcup_image {aT rT I} (P : set aT) (f : aT → I) (F : I → set rT) :
\bigcup_(x in f @` P) F x = \bigcup_(x in P) F (f x).
Lemma bigcap_image {aT rT I} (P : set aT) (f : aT → I) (F : I → set rT) :
\bigcap_(x in f @` P) F x = \bigcap_(x in P) F (f x).
Lemma bigcup_fset {I : choiceType} {U : Type}
(F : I → set U) (X : {fset I}) :
\bigcup_(i in [set i | i \in X]) F i = \big[setU/set0]_(i <- X) F i :> set U.
Lemma bigcap_fset {I : choiceType} {U : Type}
(F : I → set U) (X : {fset I}) :
\bigcap_(i in [set i | i \in X]) F i = \big[setI/setT]_(i <- X) F i :> set U.
Lemma bigcup_fsetU1 {T U : choiceType} (F : T → set U) (x : T) (X : {fset T}) :
\bigcup_(i in [set j | j \in x |` X]%fset) F i =
F x `|` \bigcup_(i in [set j | j \in X]) F i.
Lemma bigcap_fsetU1 {T U : choiceType} (F : T → set U) (x : T) (X : {fset T}) :
\bigcap_(i in [set j | j \in x |` X]%fset) F i =
F x `&` \bigcap_(i in [set j | j \in X]) F i.
Lemma bigcup_fsetD1 {T U : choiceType} (x : T) (F : T → set U) (X : {fset T}) :
x \in X →
\bigcup_(i in [set i | i \in X]%fset) F i =
F x `|` \bigcup_(i in [set i | i \in X `\ x]%fset) F i.
Arguments bigcup_fsetD1 {T U} x.
Lemma bigcap_fsetD1 {T U : choiceType} (x : T) (F : T → set U) (X : {fset T}) :
x \in X →
\bigcap_(i in [set i | i \in X]%fset) F i =
F x `&` \bigcap_(i in [set i | i \in X `\ x]%fset) F i.
Arguments bigcup_fsetD1 {T U} x.
Section bigcup_set.
Variables (T : choiceType) (U : Type).
Lemma bigcup_set_cond (s : seq T) (f : T → set U) (P : pred T) :
\bigcup_(t in [set x | (x \in s) && P x]) (f t) =
\big[setU/set0]_(t <- s | P t) (f t).
Lemma bigcup_set (s : seq T) (f : T → set U) :
\bigcup_(t in [set x | x \in s]) (f t) = \big[setU/set0]_(t <- s) (f t).
Lemma bigcap_set_cond (s : seq T) (f : T → set U) (P : pred T) :
\bigcap_(t in [set x | (x \in s) && P x]) (f t) =
\big[setI/setT]_(t <- s | P t) (f t).
Lemma bigcap_set (s : seq T) (f : T → set U) :
\bigcap_(t in [set x | x \in s]) (f t) = \big[setI/setT]_(t <- s) (f t).
End bigcup_set.
Section bigop_nat_lemmas.
Context {T : Type}.
Implicit Types (A : set T) (F : nat → set T).
Lemma bigcup_mkord n F :
\bigcup_(i in [set k | (k < n)%N]) F i = \big[setU/set0]_(i < n) F i.
Lemma bigcap_mkord n F :
\bigcap_(i in [set k | (k < n)%N]) F i = \big[setI/setT]_(i < n) F i.
Lemma bigcup_splitn n F :
\bigcup_i F i = \big[setU/set0]_(i < n) F i `|` \bigcup_i F (n + i)%N.
Lemma bigcap_splitn n F :
\bigcap_i F i = \big[setI/setT]_(i < n) F i `&` \bigcap_i F (n + i)%N.
Lemma subset_bigsetU F :
{homo (fun n ⇒ \big[setU/set0]_(i < n) F i) : n m / (n ≤ m)%N >-> n `<=` m}.
Lemma subset_bigsetI F :
{homo (fun n ⇒ \big[setI/setT]_(i < n) F i) : n m / (n ≤ m)%N >-> m `<=` n}.
Lemma subset_bigsetU_cond (P : pred nat) F :
{homo (fun n ⇒ \big[setU/set0]_(i < n | P i) F i)
: n m / (n ≤ m)%N >-> n `<=` m}.
Lemma subset_bigsetI_cond (P : pred nat) F :
{homo (fun n ⇒ \big[setI/setT]_(i < n | P i) F i)
: n m / (n ≤ m)%N >-> m `<=` n}.
End bigop_nat_lemmas.
Definition is_subset1 {T} (A : set T) := ∀ x y, A x → A y → x = y.
Definition is_fun {T1 T2} (f : T1 → T2 → Prop) := Logic.all (is_subset1 \o f).
Definition is_total {T1 T2} (f : T1 → T2 → Prop) := Logic.all (nonempty \o f).
Definition is_totalfun {T1 T2} (f : T1 → T2 → Prop) :=
∀ x, f x !=set0 ∧ is_subset1 (f x).
Definition xget {T : choiceType} x0 (P : set T) : T :=
if pselect (∃ x : T, `[<P x>]) isn't left exP then x0
else projT1 (sigW exP).
CoInductive xget_spec {T : choiceType} x0 (P : set T) : T → Prop → Type :=
| XGetSome x of x = xget x0 P & P x : xget_spec x0 P x True
| XGetNone of (∀ x, ¬ P x) : xget_spec x0 P x0 False.
Lemma xgetP {T : choiceType} x0 (P : set T) :
xget_spec x0 P (xget x0 P) (P (xget x0 P)).
Lemma xgetPex {T : choiceType} x0 (P : set T) : (∃ x, P x) → P (xget x0 P).
Lemma xgetI {T : choiceType} x0 (P : set T) (x : T): P x → P (xget x0 P).
Lemma xget_subset1 {T : choiceType} x0 (P : set T) (x : T) :
P x → is_subset1 P → xget x0 P = x.
Lemma xget_unique {T : choiceType} x0 (P : set T) (x : T) :
P x → (∀ y, P y → y = x) → xget x0 P = x.
Lemma xgetPN {T : choiceType} x0 (P : set T) :
(∀ x, ¬ P x) → xget x0 P = x0.
Definition fun_of_rel {aT} {rT : choiceType} (f0 : aT → rT)
(f : aT → rT → Prop) := fun x ⇒ xget (f0 x) (f x).
Lemma fun_of_relP {aT} {rT : choiceType} (f : aT → rT → Prop) (f0 : aT → rT) a :
f a !=set0 → f a (fun_of_rel f0 f a).
Lemma fun_of_rel_uniq {aT} {rT : choiceType}
(f : aT → rT → Prop) (f0 : aT → rT) a :
is_subset1 (f a) → ∀ b, f a b → fun_of_rel f0 f a = b.
Definition mem_set T (A : set T) (u : T) (a : A u) : u \in A :=
eq_ind_r id a (in_setE A u).
Lemma forall_sig T (A : set T) (P : {x | x \in A} → Prop) :
(∀ u : {x | x \in A}, P u) =
(∀ u : T, ∀ (a : A u), P (exist _ u (mem_set a))).
Module Pointed.
Definition point_of (T : Type) := T.
Record class_of (T : Type) := Class {
base : Choice.class_of T;
mixin : point_of T
}.
Section ClassDef.
Structure type := Pack { sort; _ : class_of sort }.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c := cT return class_of cT in c.
Definition clone c of phant_id class c := @Pack T c.
Let xT := let: Pack T _ := cT in T.
Notation xclass := (class : class_of xT).
Definition pack m :=
fun bT b of phant_id (Choice.class bT) b ⇒ @Pack T (Class b m).
Definition eqType := @Equality.Pack cT xclass.
Definition choiceType := @Choice.Pack cT xclass.
End ClassDef.
Module Exports.
Coercion sort : type >-> Sortclass.
Coercion base : class_of >-> Choice.class_of.
Coercion mixin : class_of >-> point_of.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Notation pointedType := type.
Notation PointedType T m := (@pack T m _ _ idfun).
Notation "[ 'pointedType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
(at level 0, format "[ 'pointedType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'pointedType' 'of' T ]" := (@clone T _ _ id)
(at level 0, format "[ 'pointedType' 'of' T ]") : form_scope.
End Exports.
End Pointed.
Export Pointed.Exports.
Definition point {M : pointedType} : M := Pointed.mixin (Pointed.class M).
Canonical arrow_pointedType (T : Type) (T' : pointedType) :=
PointedType (T → T') (fun⇒ point).
Definition dep_arrow_pointedType (T : Type) (T' : T → pointedType) :=
Pointed.Pack
(Pointed.Class (dep_arrow_choiceClass T') (fun i ⇒ @point (T' i))).
Canonical bool_pointedType := PointedType bool false.
Canonical Prop_pointedType := PointedType Prop False.
Canonical nat_pointedType := PointedType nat 0%N.
Canonical prod_pointedType (T T' : pointedType) :=
PointedType (T × T') (point, point).
Canonical matrix_pointedType m n (T : pointedType) :=
PointedType 'M[T]_(m, n) (\matrix_(_, _) point)%R.
Notation get := (xget point).
Section PointedTheory.
Context {T : pointedType}.
Lemma getPex (P : set T) : (∃ x, P x) → P (get P).
Lemma getI (P : set T) (x : T): P x → P (get P).
Lemma get_subset1 (P : set T) (x : T) : P x → is_subset1 P → get P = x.
Lemma get_unique (P : set T) (x : T) :
P x → (∀ y, P y → y = x) → get P = x.
Lemma getPN (P : set T) : (∀ x, ¬ P x) → get P = point.
End PointedTheory.
Definition patch {U: Type} {V} (dflt : U → V) (A : set U) (f : U → V) u :=
if u \in A then f u else dflt u.
Notation restrict := (patch (fun⇒ point)).
Notation "f \|_ D" := (restrict D) : fun_scope.
Definition restrict_dep {U V} (A : set U) (f : U → V)
(u : { x : U | x \in A }) : V := f (projT1 u).
Arguments restrict_dep {U V} A.
Definition extend_dep {U} {V : pointedType} {A : set U}
(f : {x | x \in A } → V) (u : U) :=
if pselect (u \in A) is left w then f (exist _ u w) else point.
Lemma restrict_depE T T' (B : set T) x (f : T → T') (xB : B x) :
restrict_dep B f (exist _ x (mem_set xB)) = f x.
Arguments restrict_depE {T T'} B x.
Lemma in_setP {U} (A : set U) (P : U → Prop) :
{in A, ∀ x, P x} ↔ ∀ x, A x → P x.
Lemma in_set2P {U V} (A : set U) (B : set V) (P : U → V → Prop) :
{in A & B, ∀ x y, P x y} ↔ (∀ x y, A x → B y → P x y).
Lemma fun_eq_inP {U V} (f g : U → V) (A : set U) :
{in A, f =1 g} ↔ restrict_dep A f = restrict_dep A g.
Section Restrictions.
Context {U : Type} {V : pointedType} (A : set U).
Open Scope fun_scope.
Lemma extend_restrict_dep : extend_dep \o restrict_dep = restrict.
Lemma extend_depK : cancel extend_dep restrict_dep.
Lemma restrict_extend_dep : restrict_dep \o extend_dep = id.
Lemma restrict_dep_restrict : restrict_dep \o restrict = restrict_dep.
Lemma restrict_dep_setT : [set of restrict_dep] = setT.
End Restrictions.
Section partitions.
Definition trivIset T I (D : set I) (F : I → set T) :=
∀ i j : I, D i → D j → F i `&` F j !=set0 → i = j.
Lemma trivIsetP {T} {I : eqType} {D : set I} {F : I → set T} :
trivIset D F ↔
∀ i j : I, D i → D j → i != j → F i `&` F j = set0.
Lemma trivIset_bigsetUI T (D : {pred nat}) (F : nat → set T) : trivIset D F →
∀ n m, D m → n ≤ m → \big[setU/set0]_(i < n | D i) F i `&` F m = set0.
Lemma trivIset_setI T I D (F : I → set T) X :
trivIset D F → trivIset D (fun i ⇒ X `&` F i).
Definition cover T I D (F : I → set T) := \bigcup_(i in D) F i.
Lemma cover_restr T I D' D (F : I → set T) :
D `<=` D' → (∀ i, D' i → ¬ D i → F i = set0) →
cover D F = cover D' F.
Lemma eqcover_r T I D (F G : I → set T) :
[set F i | i in D] = [set G i | i in D] →
cover D F = cover D G.
Definition partition T I D (F : I → set T) (A : set T) :=
[/\ cover D F = A, trivIset D F & ∀ i, D i → F i !=set0].
Definition pblock_index T (I : pointedType) D (F : I → set T) (x : T) :=
get (fun i ⇒ D i ∧ F i x).
Definition pblock T (I : pointedType) D (F : I → set T) (x : T) :=
F (pblock_index D F x).
[disjoint A & B]%fset = [disjoint [set x | x \in A] & [set x | x \in B]].
Section SetFset.
Context {T : choiceType}.
Implicit Types (x y : T) (A B : {fset T}).
Lemma set_fset0 : [set y : T | y \in fset0] = set0.
Lemma set_fset1 x : [set y | y \in [fset x]%fset] = [set x].
Lemma set_fsetI A B :
[set x | x \in (A `&` B)%fset] = [set x | x \in A] `&` [set x | x \in B].
Lemma set_fsetU A B :
[set x | x \in (A `|` B)%fset] = [set x | x \in A] `|` [set x | x \in B].
Lemma set_fsetU1 x A : [set y | y \in (x |` A)%fset] = x |` [set x | x \in A].
Lemma set_fsetD A B :
[set x | x \in (A `\` B)%fset] = [set x | x \in A] `\` [set x | x \in B].
Lemma set_fsetD1 A x : [set y | y \in (A `\ x)%fset] = [set x | x \in A] `\ x.
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 image_lemmas.
Context {aT rT : Type}.
Implicit Types (A B : set aT) (f : aT → rT) (Y : set rT).
Lemma imageP f A a : A a → (f @` A) (f a).
Lemma image_inj {f A a} : injective f → (f @` A) (f a) = A a.
Lemma image_id A : id @` A = A.
Lemma image_setU f A B : f @` (A `|` B) = f @` A `|` f @` B.
Lemma image_set0 f : f @` set0 = set0.
Lemma image_set0_set0 A f : f @` A = set0 → A = set0.
Lemma image_set1 f t : f @` [set t] = [set f t].
Lemma subset_set1 A a : A `<=` [set a] → A = set0 ∨ A = [set a].
Lemma sub_image_setI f A B : f @` (A `&` B) `<=` f @` A `&` f @` B.
Lemma nonempty_image f A : f @` A !=set0 → A !=set0.
Lemma image_subset f A B : A `<=` B → f @` A `<=` f @` B.
Lemma preimage_set0 f : f @^-1` set0 = set0.
Lemma nonempty_preimage f Y : f @^-1` Y !=set0 → Y !=set0.
Lemma preimage_image f A : A `<=` f @^-1` (f @` A).
Lemma image_preimage_subset f Y : f @` (f @^-1` Y) `<=` Y.
Lemma image_preimage f Y : f @` setT = setT → f @` (f @^-1` Y) = Y.
Lemma eq_imagel T1 T2 (A : set T1) (f f' : T1 → T2) :
(∀ x, A x → f x = f' x) → f @` A = f' @` A.
Lemma preimage_setU f Y1 Y2 : f @^-1` (Y1 `|` Y2) = f @^-1` Y1 `|` f @^-1` Y2.
Lemma preimage_setI f Y1 Y2 : f @^-1` (Y1 `&` Y2) = f @^-1` Y1 `&` f @^-1` Y2.
Lemma preimage_setC f Y : ~` (f @^-1` Y) = f @^-1` (~` Y).
Lemma preimage_subset f Y1 Y2 : Y1 `<=` Y2 → f @^-1` Y1 `<=` f @^-1` Y2.
Lemma nonempty_preimage_setI f Y1 Y2 :
(f @^-1` (Y1 `&` Y2)) !=set0 ↔ (f @^-1` Y1 `&` f @^-1` Y2) !=set0.
Lemma preimage_bigcup {I} (P : set I) f (F : I → set rT) :
f @^-1` (\bigcup_ (i in P) F i) = \bigcup_(i in P) (f @^-1` F i).
Lemma preimage_bigcap {I} (P : set I) f (F : I → set rT) :
f @^-1` (\bigcap_ (i in P) F i) = \bigcap_(i in P) (f @^-1` F i).
End image_lemmas.
Arguments sub_image_setI {aT rT f A B} t _.
Lemma image_comp T1 T2 T3 (f : T1 → T2) (g : T2 → T3) A :
g @` (f @` A) = (g \o f) @` A.
Section bigop_lemmas.
Context {T I : Type}.
Implicit Types (A : set T) (i : I) (P : set I) (F G : I → set T).
Lemma bigcup_sup i P F : P i → F i `<=` \bigcup_(j in P) F j.
Lemma bigcap_inf i P F : P i → \bigcap_(j in P) F j `<=` F i.
Lemma subset_bigcup_r P : {homo (fun x : I → set T ⇒ \bigcup_(i in P) x i)
: F G / [set F i | i in P] `<=` [set G i | i in P] >-> F `<=` G}.
Lemma subset_bigcap_r P : {homo (fun x : I → set T ⇒ \bigcap_(i in P) x i)
: F G / [set F i | i in P] `<=` [set G i | i in P] >-> G `<=` F}.
Lemma eq_bigcupr P F G : (∀ i, P i → F i = G i) →
\bigcup_(i in P) F i = \bigcup_(i in P) G i.
Lemma eq_bigcapr P F G : (∀ i, P i → F i = G i) →
\bigcap_(i in P) F i = \bigcap_(i in P) G i.
Lemma setC_bigcup P F : ~` (\bigcup_(i in P) F i) = \bigcap_(i in P) ~` F i.
Lemma setC_bigcap P F : ~` (\bigcap_(i in P) (F i)) = \bigcup_(i in P) ~` F i.
Lemma eq_bigcupl P Q F : P `<=>` Q →
\bigcup_(i in P) F i = \bigcup_(i in Q) F i.
Lemma eq_bigcapl P Q F : P `<=>` Q →
\bigcap_(i in P) F i = \bigcap_(i in Q) F i.
Lemma eq_bigcup P Q F G : P `<=>` Q → (∀ i, P i → F i = G i) →
\bigcup_(i in P) F i = \bigcup_(i in Q) G i.
Lemma eq_bigcap P Q F G : P `<=>` Q → (∀ i, P i → F i = G i) →
\bigcap_(i in P) F i = \bigcap_(i in Q) G i.
Lemma bigcupU P F G : \bigcup_(i in P) (F i `|` G i) =
(\bigcup_(i in P) F i) `|` (\bigcup_(i in P) G i).
Lemma bigcapI P F G : \bigcap_(i in P) (F i `&` G i) =
(\bigcap_(i in P) F i) `&` (\bigcap_(i in P) G i).
Lemma bigcup_const P A : P !=set0 → \bigcup_(_ in P) A = A.
Lemma bigcap_const P A : P !=set0 → \bigcap_(_ in P) A = A.
Lemma bigcapIl P F A : P !=set0 →
\bigcap_(i in P) (F i `&` A) = \bigcap_(i in P) F i `&` A.
Lemma bigcapIr P F A : P !=set0 →
\bigcap_(i in P) (A `&` F i) = A `&` \bigcap_(i in P) F i.
Lemma bigcupUl P F A : P !=set0 →
\bigcup_(i in P) (F i `|` A) = \bigcup_(i in P) F i `|` A.
Lemma bigcupUr P F A : P !=set0 →
\bigcup_(i in P) (A `|` F i) = A `|` \bigcup_(i in P) F i.
Lemma bigcup_set0 F : \bigcup_(i in set0) F i = set0.
Lemma bigcup_set1 F i : \bigcup_(j in [set i]) F j = F i.
Lemma bigcap_set0 F : \bigcap_(i in set0) F i = setT.
Lemma bigcap_set1 F i : \bigcap_(j in [set i]) F j = F i.
Lemma bigcup_nonempty P F :
(\bigcup_(i in P) F i !=set0) ↔ exists2 i, P i & F i !=set0.
Lemma bigcup0 P F :
(∀ i, P i → F i = set0) → \bigcup_(i in P) F i = set0.
Lemma bigcap0 P F :
(exists2 i, P i & F i = set0) → \bigcap_(i in P) F i = set0.
Lemma bigcapT P F :
(∀ i, P i → F i = setT) → \bigcap_(i in P) F i = setT.
Lemma bigcupT P F :
(exists2 i, P i & F i = setT) → \bigcup_(i in P) F i = setT.
Lemma bigcup0P P F :
(\bigcup_(i in P) F i = set0) ↔ ∀ i, P i → F i = set0.
Lemma bigcapTP P F :
(\bigcap_(i in P) F i = setT) ↔ ∀ i, P i → F i = setT.
Lemma setI_bigcupr F P A :
A `&` \bigcup_(i in P) F i = \bigcup_(i in P) (A `&` F i).
Lemma setI_bigcupl F P A :
\bigcup_(i in P) F i `&` A = \bigcup_(i in P) (F i `&` A).
Lemma setU_bigcapr F P A :
A `|` \bigcap_(i in P) F i = \bigcap_(i in P) (A `|` F i).
Lemma setU_bigcapl F P A :
\bigcap_(i in P) F i `|` A = \bigcap_(i in P) (F i `|` A).
Lemma bigcup_mkcond F P :
\bigcup_(i in P) F i = \bigcup_i if `[< P i >] then F i else set0.
Lemma bigcap_mkcond F P :
\bigcap_(i in P) F i = \bigcap_i if `[< P i >] then F i else setT.
Lemma bigcup_imset1 P (f : I → T) : \bigcup_(x in P) [set f x] = f @` P.
Lemma bigcup_setU F (X Y : set I) :
\bigcup_(i in X `|` Y) F i = \bigcup_(i in X) F i `|` \bigcup_(i in Y) F i.
Lemma bigcap_setU F (X Y : set I) :
\bigcap_(i in X `|` Y) F i = \bigcap_(i in X) F i `&` \bigcap_(i in Y) F i.
Lemma bigcup_setU1 F (x : I) (X : set I) :
\bigcup_(i in x |` X) F i = F x `|` \bigcup_(i in X) F i.
Lemma bigcap_setU1 F (x : I) (X : set I) :
\bigcap_(i in x |` X) F i = F x `&` \bigcap_(i in X) F i.
Lemma bigcup_setD1 (x : I) F (X : set I) : X x →
\bigcup_(i in X) F i = F x `|` \bigcup_(i in X `\ x) F i.
Lemma bigcap_setD1 (x : I) F (X : set I) : X x →
\bigcap_(i in X) F i = F x `&` \bigcap_(i in X `\ x) F i.
Lemma setC_bigsetU U (s : seq T) (f : T → set U) (P : pred T) :
(~` \big[setU/set0]_(t <- s | P t) f t) = \big[setI/setT]_(t <- s | P t) ~` f t.
Lemma setC_bigsetI U (s : seq T) (f : T → set U) (P : pred T) :
(~` \big[setI/setT]_(t <- s | P t) f t) = \big[setU/set0]_(t <- s | P t) ~` f t.
End bigop_lemmas.
Arguments bigcup_setD1 {T I} x.
Arguments bigcap_setD1 {T I} x.
Lemma bigcup_image {aT rT I} (P : set aT) (f : aT → I) (F : I → set rT) :
\bigcup_(x in f @` P) F x = \bigcup_(x in P) F (f x).
Lemma bigcap_image {aT rT I} (P : set aT) (f : aT → I) (F : I → set rT) :
\bigcap_(x in f @` P) F x = \bigcap_(x in P) F (f x).
Lemma bigcup_fset {I : choiceType} {U : Type}
(F : I → set U) (X : {fset I}) :
\bigcup_(i in [set i | i \in X]) F i = \big[setU/set0]_(i <- X) F i :> set U.
Lemma bigcap_fset {I : choiceType} {U : Type}
(F : I → set U) (X : {fset I}) :
\bigcap_(i in [set i | i \in X]) F i = \big[setI/setT]_(i <- X) F i :> set U.
Lemma bigcup_fsetU1 {T U : choiceType} (F : T → set U) (x : T) (X : {fset T}) :
\bigcup_(i in [set j | j \in x |` X]%fset) F i =
F x `|` \bigcup_(i in [set j | j \in X]) F i.
Lemma bigcap_fsetU1 {T U : choiceType} (F : T → set U) (x : T) (X : {fset T}) :
\bigcap_(i in [set j | j \in x |` X]%fset) F i =
F x `&` \bigcap_(i in [set j | j \in X]) F i.
Lemma bigcup_fsetD1 {T U : choiceType} (x : T) (F : T → set U) (X : {fset T}) :
x \in X →
\bigcup_(i in [set i | i \in X]%fset) F i =
F x `|` \bigcup_(i in [set i | i \in X `\ x]%fset) F i.
Arguments bigcup_fsetD1 {T U} x.
Lemma bigcap_fsetD1 {T U : choiceType} (x : T) (F : T → set U) (X : {fset T}) :
x \in X →
\bigcap_(i in [set i | i \in X]%fset) F i =
F x `&` \bigcap_(i in [set i | i \in X `\ x]%fset) F i.
Arguments bigcup_fsetD1 {T U} x.
Section bigcup_set.
Variables (T : choiceType) (U : Type).
Lemma bigcup_set_cond (s : seq T) (f : T → set U) (P : pred T) :
\bigcup_(t in [set x | (x \in s) && P x]) (f t) =
\big[setU/set0]_(t <- s | P t) (f t).
Lemma bigcup_set (s : seq T) (f : T → set U) :
\bigcup_(t in [set x | x \in s]) (f t) = \big[setU/set0]_(t <- s) (f t).
Lemma bigcap_set_cond (s : seq T) (f : T → set U) (P : pred T) :
\bigcap_(t in [set x | (x \in s) && P x]) (f t) =
\big[setI/setT]_(t <- s | P t) (f t).
Lemma bigcap_set (s : seq T) (f : T → set U) :
\bigcap_(t in [set x | x \in s]) (f t) = \big[setI/setT]_(t <- s) (f t).
End bigcup_set.
Section bigop_nat_lemmas.
Context {T : Type}.
Implicit Types (A : set T) (F : nat → set T).
Lemma bigcup_mkord n F :
\bigcup_(i in [set k | (k < n)%N]) F i = \big[setU/set0]_(i < n) F i.
Lemma bigcap_mkord n F :
\bigcap_(i in [set k | (k < n)%N]) F i = \big[setI/setT]_(i < n) F i.
Lemma bigcup_splitn n F :
\bigcup_i F i = \big[setU/set0]_(i < n) F i `|` \bigcup_i F (n + i)%N.
Lemma bigcap_splitn n F :
\bigcap_i F i = \big[setI/setT]_(i < n) F i `&` \bigcap_i F (n + i)%N.
Lemma subset_bigsetU F :
{homo (fun n ⇒ \big[setU/set0]_(i < n) F i) : n m / (n ≤ m)%N >-> n `<=` m}.
Lemma subset_bigsetI F :
{homo (fun n ⇒ \big[setI/setT]_(i < n) F i) : n m / (n ≤ m)%N >-> m `<=` n}.
Lemma subset_bigsetU_cond (P : pred nat) F :
{homo (fun n ⇒ \big[setU/set0]_(i < n | P i) F i)
: n m / (n ≤ m)%N >-> n `<=` m}.
Lemma subset_bigsetI_cond (P : pred nat) F :
{homo (fun n ⇒ \big[setI/setT]_(i < n | P i) F i)
: n m / (n ≤ m)%N >-> m `<=` n}.
End bigop_nat_lemmas.
Definition is_subset1 {T} (A : set T) := ∀ x y, A x → A y → x = y.
Definition is_fun {T1 T2} (f : T1 → T2 → Prop) := Logic.all (is_subset1 \o f).
Definition is_total {T1 T2} (f : T1 → T2 → Prop) := Logic.all (nonempty \o f).
Definition is_totalfun {T1 T2} (f : T1 → T2 → Prop) :=
∀ x, f x !=set0 ∧ is_subset1 (f x).
Definition xget {T : choiceType} x0 (P : set T) : T :=
if pselect (∃ x : T, `[<P x>]) isn't left exP then x0
else projT1 (sigW exP).
CoInductive xget_spec {T : choiceType} x0 (P : set T) : T → Prop → Type :=
| XGetSome x of x = xget x0 P & P x : xget_spec x0 P x True
| XGetNone of (∀ x, ¬ P x) : xget_spec x0 P x0 False.
Lemma xgetP {T : choiceType} x0 (P : set T) :
xget_spec x0 P (xget x0 P) (P (xget x0 P)).
Lemma xgetPex {T : choiceType} x0 (P : set T) : (∃ x, P x) → P (xget x0 P).
Lemma xgetI {T : choiceType} x0 (P : set T) (x : T): P x → P (xget x0 P).
Lemma xget_subset1 {T : choiceType} x0 (P : set T) (x : T) :
P x → is_subset1 P → xget x0 P = x.
Lemma xget_unique {T : choiceType} x0 (P : set T) (x : T) :
P x → (∀ y, P y → y = x) → xget x0 P = x.
Lemma xgetPN {T : choiceType} x0 (P : set T) :
(∀ x, ¬ P x) → xget x0 P = x0.
Definition fun_of_rel {aT} {rT : choiceType} (f0 : aT → rT)
(f : aT → rT → Prop) := fun x ⇒ xget (f0 x) (f x).
Lemma fun_of_relP {aT} {rT : choiceType} (f : aT → rT → Prop) (f0 : aT → rT) a :
f a !=set0 → f a (fun_of_rel f0 f a).
Lemma fun_of_rel_uniq {aT} {rT : choiceType}
(f : aT → rT → Prop) (f0 : aT → rT) a :
is_subset1 (f a) → ∀ b, f a b → fun_of_rel f0 f a = b.
Definition mem_set T (A : set T) (u : T) (a : A u) : u \in A :=
eq_ind_r id a (in_setE A u).
Lemma forall_sig T (A : set T) (P : {x | x \in A} → Prop) :
(∀ u : {x | x \in A}, P u) =
(∀ u : T, ∀ (a : A u), P (exist _ u (mem_set a))).
Module Pointed.
Definition point_of (T : Type) := T.
Record class_of (T : Type) := Class {
base : Choice.class_of T;
mixin : point_of T
}.
Section ClassDef.
Structure type := Pack { sort; _ : class_of sort }.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c := cT return class_of cT in c.
Definition clone c of phant_id class c := @Pack T c.
Let xT := let: Pack T _ := cT in T.
Notation xclass := (class : class_of xT).
Definition pack m :=
fun bT b of phant_id (Choice.class bT) b ⇒ @Pack T (Class b m).
Definition eqType := @Equality.Pack cT xclass.
Definition choiceType := @Choice.Pack cT xclass.
End ClassDef.
Module Exports.
Coercion sort : type >-> Sortclass.
Coercion base : class_of >-> Choice.class_of.
Coercion mixin : class_of >-> point_of.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Notation pointedType := type.
Notation PointedType T m := (@pack T m _ _ idfun).
Notation "[ 'pointedType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
(at level 0, format "[ 'pointedType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'pointedType' 'of' T ]" := (@clone T _ _ id)
(at level 0, format "[ 'pointedType' 'of' T ]") : form_scope.
End Exports.
End Pointed.
Export Pointed.Exports.
Definition point {M : pointedType} : M := Pointed.mixin (Pointed.class M).
Canonical arrow_pointedType (T : Type) (T' : pointedType) :=
PointedType (T → T') (fun⇒ point).
Definition dep_arrow_pointedType (T : Type) (T' : T → pointedType) :=
Pointed.Pack
(Pointed.Class (dep_arrow_choiceClass T') (fun i ⇒ @point (T' i))).
Canonical bool_pointedType := PointedType bool false.
Canonical Prop_pointedType := PointedType Prop False.
Canonical nat_pointedType := PointedType nat 0%N.
Canonical prod_pointedType (T T' : pointedType) :=
PointedType (T × T') (point, point).
Canonical matrix_pointedType m n (T : pointedType) :=
PointedType 'M[T]_(m, n) (\matrix_(_, _) point)%R.
Notation get := (xget point).
Section PointedTheory.
Context {T : pointedType}.
Lemma getPex (P : set T) : (∃ x, P x) → P (get P).
Lemma getI (P : set T) (x : T): P x → P (get P).
Lemma get_subset1 (P : set T) (x : T) : P x → is_subset1 P → get P = x.
Lemma get_unique (P : set T) (x : T) :
P x → (∀ y, P y → y = x) → get P = x.
Lemma getPN (P : set T) : (∀ x, ¬ P x) → get P = point.
End PointedTheory.
Definition patch {U: Type} {V} (dflt : U → V) (A : set U) (f : U → V) u :=
if u \in A then f u else dflt u.
Notation restrict := (patch (fun⇒ point)).
Notation "f \|_ D" := (restrict D) : fun_scope.
Definition restrict_dep {U V} (A : set U) (f : U → V)
(u : { x : U | x \in A }) : V := f (projT1 u).
Arguments restrict_dep {U V} A.
Definition extend_dep {U} {V : pointedType} {A : set U}
(f : {x | x \in A } → V) (u : U) :=
if pselect (u \in A) is left w then f (exist _ u w) else point.
Lemma restrict_depE T T' (B : set T) x (f : T → T') (xB : B x) :
restrict_dep B f (exist _ x (mem_set xB)) = f x.
Arguments restrict_depE {T T'} B x.
Lemma in_setP {U} (A : set U) (P : U → Prop) :
{in A, ∀ x, P x} ↔ ∀ x, A x → P x.
Lemma in_set2P {U V} (A : set U) (B : set V) (P : U → V → Prop) :
{in A & B, ∀ x y, P x y} ↔ (∀ x y, A x → B y → P x y).
Lemma fun_eq_inP {U V} (f g : U → V) (A : set U) :
{in A, f =1 g} ↔ restrict_dep A f = restrict_dep A g.
Section Restrictions.
Context {U : Type} {V : pointedType} (A : set U).
Open Scope fun_scope.
Lemma extend_restrict_dep : extend_dep \o restrict_dep = restrict.
Lemma extend_depK : cancel extend_dep restrict_dep.
Lemma restrict_extend_dep : restrict_dep \o extend_dep = id.
Lemma restrict_dep_restrict : restrict_dep \o restrict = restrict_dep.
Lemma restrict_dep_setT : [set of restrict_dep] = setT.
End Restrictions.
Section partitions.
Definition trivIset T I (D : set I) (F : I → set T) :=
∀ i j : I, D i → D j → F i `&` F j !=set0 → i = j.
Lemma trivIsetP {T} {I : eqType} {D : set I} {F : I → set T} :
trivIset D F ↔
∀ i j : I, D i → D j → i != j → F i `&` F j = set0.
Lemma trivIset_bigsetUI T (D : {pred nat}) (F : nat → set T) : trivIset D F →
∀ n m, D m → n ≤ m → \big[setU/set0]_(i < n | D i) F i `&` F m = set0.
Lemma trivIset_setI T I D (F : I → set T) X :
trivIset D F → trivIset D (fun i ⇒ X `&` F i).
Definition cover T I D (F : I → set T) := \bigcup_(i in D) F i.
Lemma cover_restr T I D' D (F : I → set T) :
D `<=` D' → (∀ i, D' i → ¬ D i → F i = set0) →
cover D F = cover D' F.
Lemma eqcover_r T I D (F G : I → set T) :
[set F i | i in D] = [set G i | i in D] →
cover D F = cover D G.
Definition partition T I D (F : I → set T) (A : set T) :=
[/\ cover D F = A, trivIset D F & ∀ i, D i → F i !=set0].
Definition pblock_index T (I : pointedType) D (F : I → set T) (x : T) :=
get (fun 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
Lemma trivIset_sets T I D (F : I → set T) :
trivIset D F → trivIset [set F i | i in D] id.
Lemma trivIset_restr T I D' D (F : I → set T) :
D `<=` D' -> (forall i, D i -> ~ D' i -> F i !=set0) ->
D `<=` D' → (∀ i, D' i → ¬ D i → F i = set0) →
trivIset D F = trivIset D' F.
Lemma perm_eq_trivIset {T : eqType} (s1 s2 : seq (set T)) (D : set nat) :
[set k | (k < size s1)%N] `<=` D → perm_eq s1 s2 →
trivIset D (fun i ⇒ nth set0 s1 i) → trivIset D (fun i ⇒ nth set0 s2 i).
End partitions.
Definition total_on T (A : set T) (R : T → T → Prop) :=
∀ s t, A s → A t → R s t ∨ R t s.
Section ZL.
Variable (T : Type) (t0 : T) (R : T → T → Prop).
Hypothesis (Rrefl : ∀ t, R t t).
Hypothesis (Rtrans : ∀ r s t, R r s → R s t → R r t).
Hypothesis (Rantisym : ∀ s t, R s t → R t s → s = t).
Hypothesis (tot_lub : ∀ A : set T, total_on A R → ∃ t,
(∀ s, A s → R s t) ∧ ∀ r, (∀ s, A s → R s r) → R t r).
Hypothesis (Rsucc : ∀ s, ∃ t, R s t ∧ s ≠ t ∧
∀ r, R s r → R r t → r = s ∨ r = t).
Let Teq := @gen_eqMixin T.
Let Tch := @gen_choiceMixin T.
Let Tp := Pointed.Pack (Pointed.Class (Choice.Class Teq Tch) t0).
Let lub := fun A : {A : set T | total_on A R} ⇒
get (fun t : Tp ⇒ (∀ s, sval A s → R s t) ∧
∀ r, (∀ s, sval A s → R s r) → R t r).
Let succ := fun s ⇒ get (fun t : Tp ⇒ R s t ∧ s ≠ t ∧
∀ r, R s r → R r t → r = s ∨ r = t).
Inductive tower : set T :=
| Lub : ∀ A, sval A `<=` tower → tower (lub A)
| Succ : ∀ t, tower t → tower (succ t).
Lemma ZL' : False.
End ZL.
Lemma Zorn T (R : T → T → Prop) :
(∀ t, R t t) → (∀ r s t, R r s → R s t → R r t) →
(∀ s t, R s t → R t s → s = t) →
(∀ A : set T, total_on A R → ∃ t, ∀ s, A s → R s t) →
∃ t, ∀ s, R t s → s = t.
Definition premaximal T (R : T → T → Prop) (t : T) :=
∀ s, R t s → R s t.
Lemma ZL_preorder T (t0 : T) (R : T → T → Prop) :
(∀ t, R t t) → (∀ r s t, R r s → R s t → R r t) →
(∀ A : set T, total_on A R → ∃ t, ∀ s, A s → R s t) →
∃ t, premaximal R t.
Section UpperLowerTheory.
Import Order.TTheory.
Variables (d : unit) (T : porderType d).
Implicit Types A : set T.
Definition ubound A : set T := [set z | ∀ y, A y → (y ≤ z)%O].
Definition lbound A : set T := [set z | ∀ y, A y → (z ≤ y)%O].
Lemma ubP A x : (∀ y, A y → (y ≤ x)%O) ↔ ubound A x.
Lemma lbP A x : (∀ y, A y → (x ≤ y)%O) ↔ lbound A x.
Lemma ub_set1 x y : ubound [set x] y = (x ≤ y)%O.
Lemma lb_set1 x y : lbound [set x] y = (x ≥ y)%O.
Lemma lb_ub_set1 x y : lbound (ubound [set x]) y → (y ≤ x)%O.
Lemma ub_lb_set1 x y : ubound (lbound [set x]) y → (x ≤ y)%O.
Lemma lb_ub_refl x : lbound (ubound [set x]) x.
Lemma ub_lb_refl x : ubound (lbound [set x]) x.
Lemma ub_lb_ub A x y : ubound A y → lbound (ubound A) x → (x ≤ y)%O.
Lemma lb_ub_lb A x y : lbound A y → ubound (lbound A) x → (y ≤ x)%O.
trivIset D F = trivIset D' F.
Lemma perm_eq_trivIset {T : eqType} (s1 s2 : seq (set T)) (D : set nat) :
[set k | (k < size s1)%N] `<=` D → perm_eq s1 s2 →
trivIset D (fun i ⇒ nth set0 s1 i) → trivIset D (fun i ⇒ nth set0 s2 i).
End partitions.
Definition total_on T (A : set T) (R : T → T → Prop) :=
∀ s t, A s → A t → R s t ∨ R t s.
Section ZL.
Variable (T : Type) (t0 : T) (R : T → T → Prop).
Hypothesis (Rrefl : ∀ t, R t t).
Hypothesis (Rtrans : ∀ r s t, R r s → R s t → R r t).
Hypothesis (Rantisym : ∀ s t, R s t → R t s → s = t).
Hypothesis (tot_lub : ∀ A : set T, total_on A R → ∃ t,
(∀ s, A s → R s t) ∧ ∀ r, (∀ s, A s → R s r) → R t r).
Hypothesis (Rsucc : ∀ s, ∃ t, R s t ∧ s ≠ t ∧
∀ r, R s r → R r t → r = s ∨ r = t).
Let Teq := @gen_eqMixin T.
Let Tch := @gen_choiceMixin T.
Let Tp := Pointed.Pack (Pointed.Class (Choice.Class Teq Tch) t0).
Let lub := fun A : {A : set T | total_on A R} ⇒
get (fun t : Tp ⇒ (∀ s, sval A s → R s t) ∧
∀ r, (∀ s, sval A s → R s r) → R t r).
Let succ := fun s ⇒ get (fun t : Tp ⇒ R s t ∧ s ≠ t ∧
∀ r, R s r → R r t → r = s ∨ r = t).
Inductive tower : set T :=
| Lub : ∀ A, sval A `<=` tower → tower (lub A)
| Succ : ∀ t, tower t → tower (succ t).
Lemma ZL' : False.
End ZL.
Lemma Zorn T (R : T → T → Prop) :
(∀ t, R t t) → (∀ r s t, R r s → R s t → R r t) →
(∀ s t, R s t → R t s → s = t) →
(∀ A : set T, total_on A R → ∃ t, ∀ s, A s → R s t) →
∃ t, ∀ s, R t s → s = t.
Definition premaximal T (R : T → T → Prop) (t : T) :=
∀ s, R t s → R s t.
Lemma ZL_preorder T (t0 : T) (R : T → T → Prop) :
(∀ t, R t t) → (∀ r s t, R r s → R s t → R r t) →
(∀ A : set T, total_on A R → ∃ t, ∀ s, A s → R s t) →
∃ t, premaximal R t.
Section UpperLowerTheory.
Import Order.TTheory.
Variables (d : unit) (T : porderType d).
Implicit Types A : set T.
Definition ubound A : set T := [set z | ∀ y, A y → (y ≤ z)%O].
Definition lbound A : set T := [set z | ∀ y, A y → (z ≤ y)%O].
Lemma ubP A x : (∀ y, A y → (y ≤ x)%O) ↔ ubound A x.
Lemma lbP A x : (∀ y, A y → (x ≤ y)%O) ↔ lbound A x.
Lemma ub_set1 x y : ubound [set x] y = (x ≤ y)%O.
Lemma lb_set1 x y : lbound [set x] y = (x ≥ y)%O.
Lemma lb_ub_set1 x y : lbound (ubound [set x]) y → (y ≤ x)%O.
Lemma ub_lb_set1 x y : ubound (lbound [set x]) y → (x ≤ y)%O.
Lemma lb_ub_refl x : lbound (ubound [set x]) x.
Lemma ub_lb_refl x : ubound (lbound [set x]) x.
Lemma ub_lb_ub A x y : ubound A y → lbound (ubound A) x → (x ≤ y)%O.
Lemma lb_ub_lb A x y : lbound A y → ubound (lbound A) x → (y ≤ x)%O.
down set (i.e., generated order ideal)
i.e. down A := { x | exists y, y \in A /\ x <= y}
Real set supremum and infimum existence condition.
Definition has_ubound A := ubound A !=set0.
Definition has_sup A := A !=set0 ∧ has_ubound A.
Definition has_lbound A := lbound A !=set0.
Definition has_inf A := A !=set0 ∧ has_lbound A.
Lemma has_inf0 : ¬ has_inf (@set0 T).
Lemma has_sup0 : ¬ has_sup (@set0 T).
Lemma subset_has_lbound A B : A `<=` B → has_lbound B → has_lbound A.
Lemma subset_has_ubound A B : A `<=` B → has_ubound B → has_ubound A.
Lemma has_ub_set1 x : has_ubound [set x].
Lemma downP A x : (exists2 y, A y & (x ≤ y)%O) ↔ down A x.
Definition supremums A := ubound A `&` lbound (ubound A).
Lemma supremums_set1 x : supremums [set x] = [set x].
Lemma is_subset1_supremums A : is_subset1 (supremums A).
Definition supremum (x0 : T) A :=
if A == set0 then x0 else xget x0 (supremums A).
Definition infimums A := lbound A `&` ubound (lbound A).
Definition infimum (x0 : T) A :=
if A == set0 then x0 else xget x0 (infimums A).
Lemma infimums_set1 x : infimums [set x] = [set x].
Lemma is_subset1_infimums A : is_subset1 (infimums A).
End UpperLowerTheory.
Section UpperLowerOrderTheory.
Import Order.TTheory.
Variables (d : unit) (T : orderType d).
Implicit Types A : set T.
Lemma ge_supremum_Nmem x0 A t :
supremums A !=set0 → A t → (supremum x0 A ≥ t)%O.
Lemma le_infimum_Nmem x0 A t :
infimums A !=set0 → A t → (infimum x0 A ≤ t)%O.
End UpperLowerOrderTheory.
Lemma nat_supremums_neq0 (A : set nat) : ubound A !=set0 → supremums A !=set0.
Definition has_sup A := A !=set0 ∧ has_ubound A.
Definition has_lbound A := lbound A !=set0.
Definition has_inf A := A !=set0 ∧ has_lbound A.
Lemma has_inf0 : ¬ has_inf (@set0 T).
Lemma has_sup0 : ¬ has_sup (@set0 T).
Lemma subset_has_lbound A B : A `<=` B → has_lbound B → has_lbound A.
Lemma subset_has_ubound A B : A `<=` B → has_ubound B → has_ubound A.
Lemma has_ub_set1 x : has_ubound [set x].
Lemma downP A x : (exists2 y, A y & (x ≤ y)%O) ↔ down A x.
Definition supremums A := ubound A `&` lbound (ubound A).
Lemma supremums_set1 x : supremums [set x] = [set x].
Lemma is_subset1_supremums A : is_subset1 (supremums A).
Definition supremum (x0 : T) A :=
if A == set0 then x0 else xget x0 (supremums A).
Definition infimums A := lbound A `&` ubound (lbound A).
Definition infimum (x0 : T) A :=
if A == set0 then x0 else xget x0 (infimums A).
Lemma infimums_set1 x : infimums [set x] = [set x].
Lemma is_subset1_infimums A : is_subset1 (infimums A).
End UpperLowerTheory.
Section UpperLowerOrderTheory.
Import Order.TTheory.
Variables (d : unit) (T : orderType d).
Implicit Types A : set T.
Lemma ge_supremum_Nmem x0 A t :
supremums A !=set0 → A t → (supremum x0 A ≥ t)%O.
Lemma le_infimum_Nmem x0 A t :
infimums A !=set0 → A t → (infimum x0 A ≤ t)%O.
End UpperLowerOrderTheory.
Lemma nat_supremums_neq0 (A : set nat) : ubound A !=set0 → supremums A !=set0.
Definition meets T (F G : set (set T)) :=
∀ A B, F A → G B → A `&` B !=set0.
Notation "F `#` G" := (meets F G) : classical_set_scope.
Section meets.
Lemma meetsC T (F G : set (set T)) : F `#` G = G `#` F.
Lemma sub_meets T (F F' G G' : set (set T)) :
F `<=` F' → G `<=` G' → F' `#` G' → F `#` G.
Lemma meetsSr T (F G G' : set (set T)) :
G `<=` G' → F `#` G' → F `#` G.
Lemma meetsSl T (G F F' : set (set T)) :
F `<=` F' → F' `#` G → F `#` G.
End meets.
Fact set_display : unit.
Module SetOrder.
Module Internal.
Section SetOrder.
Context {T : Type}.
Implicit Types A B : set T.
Lemma le_def A B : `[< A `<=` B >] = (A `&` B == A).
Lemma lt_def A B : `[< A `<` B >] = (B != A) && `[< A `<=` B >].
Lemma joinKI B A : A `&` (A `|` B) = A.
Lemma meetKU B A : A `|` (A `&` B) = A.
Definition orderMixin := @MeetJoinMixin _ _ (fun A B ⇒ `[<proper A B>]) setI
setU le_def lt_def (@setIC _) (@setUC _) (@setIA _) (@setUA _) joinKI meetKU
(@setIUl _) setIid.
Lemma SetOrder_sub0set A : (set0 ≤ A)%O.
Lemma SetOrder_setTsub A : (A ≤ setT)%O.
Lemma subKI A B : B `&` (A `\` B) = set0.
Lemma joinIB A B : (A `&` B) `|` A `\` B = A.
End SetOrder.
End Internal.
Module Exports.
Canonical Internal.porderType.
Canonical Internal.latticeType.
Canonical Internal.distrLatticeType.
Canonical Internal.bLatticeType.
Canonical Internal.tbLatticeType.
Canonical Internal.bDistrLatticeType.
Canonical Internal.tbDistrLatticeType.
Canonical Internal.cbDistrLatticeType.
Canonical Internal.ctbDistrLatticeType.
Section exports.
Context {T : Type}.
Implicit Types A B : set T.
Lemma subsetEset A B : (A ≤ B)%O = (A `<=` B) :> Prop.
Lemma properEset A B : (A < B)%O = (A `<` B) :> Prop.
Lemma subEset A B : (A `\` B)%O = (A `\` B).
Lemma complEset A : (~` A)%O = ~` A.
Lemma botEset : 0%O = @set0 T.
Lemma topEset : 1%O = @setT T.
Lemma meetEset A B : (A `&` B)%O = (A `&` B).
Lemma joinEset A B : (A `|` B)%O = (A `|` B).
Lemma subsetPset A B : reflect (A `<=` B) (A ≤ B)%O.
Lemma properPset A B : reflect (A `<` B) (A < B)%O.
End exports.
End Exports.
End SetOrder.
Export SetOrder.Exports.