From mathcomp Require Import all_ssreflect ssralg matrix finmap order ssrnum.
From mathcomp Require Import ssrint interval.
From mathcomp Require Import mathcomp_extra boolp.
# Set Theory
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.
Thanks to this basic set theory, we proved Zorn's Lemma, which states
that any ordered set such that every totally ordered subset admits an
upper bound has a maximal element. We also proved an analogous version
for preorders, where maximal is replaced with premaximal: $t$ is
premaximal if whenever $t < s$ we also have $s < t$.
About the naming conventions in this file:
- use T, T', T1, T2, etc., aT (domain type), rT (return type) for names
of variables in Type (or choiceType/pointedType/porderType)
+ use the same suffix or prefix for the sets as their containing type
(e.g., A1 in T1, etc.)
+ as a consequence functions are rather of type aT -> rT
- use I, J when the type corresponds to an index
- sets are named A, B, C, D, etc., or Y when it is ostensibly an image
set (i.e., of type set rT)
- indexed sets are rather named F
Example of notations:
| Coq notations | | Meaning |
|-----------------------------:|---|:------------------------------------
| set0 |==| $\emptyset$
| [set: A] |==| the full set of elements of type A
| `` `\|` `` |==| $\cup$
| `` `&` `` |==| $\cap$
| `` `\` `` |==| set difference
| `` ~` `` |==| set complement
| `` `<=` `` |==| $\subseteq$
| `` f @` A `` |==| image by f of A
| `` f @^-1` A `` |==| preimage by f of A
| [set x] |==| the singleton set $\{x\}$
| [set~ x] |==| the complement of $\{x\}$
| [set E \| x in P] |==| the set of E with x ranging in P
| range f |==| image by f of the full set
| \big[setU/set0]_(i <- s \| P i) f i |==| finite union
| \bigcup_(k in P) F k |==| countable union
| \bigcap_(k in P) F k |==| countable intersection
| trivIset D F |==| F is a sequence of pairwise disjoint
| | | sets indexed over the domain D
Detailed documentation:
## Sets
```
set T == type of sets on T
(x \in P) == boolean membership predicate from ssrbool
for set P, available thanks to a canonical
predType T structure on sets on T
[set x : T | P] == set of points x : T such that P holds
[set x | P] == same as before with T left implicit
[set E | x in A] == set defined by the expression E for x in
set A
[set E | x in A & y in B] == same as before for E depending on 2
variables x and y in sets A and B
setT == full set
set0 == empty set
range f == the range of f, i.e., [set f x | x in setT]
[set a] == set containing only a
[set a : T] == same as before with the type of a made
explicit
A `|` B == union of A and B
a |` A == A extended with a
[set a1; a2; ..; an] == set containing only the n elements ai
A `&` B == intersection of A and B
A `*` B == product of A and B, i.e., set of pairs
(a,b) such that A a and B b
A.`1 == set of points a such that there exists b so
that A (a, b)
A.`2 == set of points a such that there exists b so
that A (b, a)
~` A == complement of A
[set~ a] == complement of [set a]
A `\` B == complement of B in A
A `\ a == A deprived of a
`I_n := [set k | k < n]
\bigcup_(i in P) F == union of the elements of the family F whose
index satisfies P
\bigcup_(i : T) F == union of the family F indexed on T
\bigcup_(i < n) F := \bigcup_(i in `I_n) F
\bigcup_i 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 := A `<=` B /\ ~ (B `<=` A)
A `<=>` B <-> double inclusion A `<=` B and B `<=` A
f @^-1` A == preimage of A by f
f @` A == image of A by f
This is a notation for `image A f`
A !=set0 := exists x, A x
[set` p] == a classical set corresponding to the
predType p
`[a, b] := [set` `[a, b]], i.e., a classical set
corresponding to the interval `[a, b]
`]a, b] := [set` `]a, b]]
`[a, b[ := [set` `[a, b[]
`]a, b[ := [set` `]a, b[]
`]-oo, b] := [set` `]-oo, b]]
`]-oo, b[ := [set` `]-oo, b[]
`[a, +oo[ := [set` `[a, +oo[]
`]a, +oo[ := [set` `]a, +oo[]
`]-oo, +oo[ := [set` `]-oo, +oo[]
is_subset1 A <-> A contains only 1 element
is_fun f <-> for each a, f a contains only 1 element
is_total f <-> for each a, f a is non empty
is_totalfun f <-> conjunction of is_fun and is_total
xget x0 P == point x in P if it exists, x0 otherwise;
P must be a set on a choiceType
fun_of_rel f0 f == function that maps x to an element of f x
if there is one, to f0 x otherwise
F `#` G <-> intersections beween elements of F an G are
all non empty
```
## 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.
```
```
$| 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)
maximal_disjoint_subcollection F A B == A is a maximal (for inclusion)
disjoint subcollection of the collection
B of elements in F : I -> set T
```
## Upper and lower bounds
```
ubound A == the set of upper bounds of the set A
lbound A == the set of lower bounds of the set A
```
Predicates to express existence conditions of supremum and infimum of sets
of real numbers:
```
has_ubound A := ubound A != set0
has_sup A := A != set0 /\ has_ubound A
has_lbound A := lbound A != set0
has_inf A := A != set0 /\ has_lbound A
isLub A m := m is a least upper bound of the set A
supremums A := set of supremums of the set A
supremum x0 A == supremum of A or x0 if A is empty
infimums A := set of infimums of the set A
infimum x0 A == infimum of A or x0 if A is empty
F `#` G := the classes of sets F and G intersect
```
## Sections
```
xsection A x == with A : set (T1 * T2) and x : T1 is the
x-section of A
ysection A y == with A : set (T1 * T2) and y : T2 is the
y-section of A
```
## 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.
Reserved Notation "[ 'set' x : T | P ]"
(
at level 0, x at level 99, only parsing).
Reserved Notation "[ 'set' x | P ]"
(
at level 0, x, P at level 99, format "[ 'set' x | P ]").
Reserved Notation "[ 'set' E | x 'in' A ]" (
at level 0, E, x at level 99,
format "[ '[hv' 'set' E '/ ' | x 'in' A ] ']'").
Reserved Notation "[ 'set' E | x 'in' A & y 'in' B ]"
(
at level 0, E, x at level 99,
format "[ '[hv' 'set' E '/ ' | x 'in' A & y 'in' B ] ']'").
Reserved Notation "[ 'set' a ]"
(
at level 0, a at level 99, format "[ 'set' a ]").
Reserved Notation "[ 'set' : T ]" (at level 0, format "[ 'set' : T ]").
Reserved Notation "[ 'set' a : T ]"
(
at level 0, a at level 99, format "[ 'set' a : T ]").
Reserved Notation "A `|` B" (
at level 52, left associativity).
Reserved Notation "a |` A" (
at level 52, left associativity).
Reserved Notation "[ 'set' a1 ; a2 ; .. ; an ]"
(
at level 0, a1 at level 99, format "[ 'set' a1 ; a2 ; .. ; an ]").
Reserved Notation "A `&` B" (
at level 48, left associativity).
Reserved Notation "A `*` B" (
at level 46, left associativity).
Reserved Notation "A `*`` B" (
at level 46, left associativity).
Reserved Notation "A ``*` B" (
at level 46, left associativity).
Reserved Notation "A .`1" (at level 2, left associativity, format "A .`1").
Reserved Notation "A .`2" (at level 2, left associativity, format "A .`2").
Reserved Notation "~` A" (
at level 35, right associativity).
Reserved Notation "[ 'set' ~ a ]" (at level 0, format "[ 'set' ~ a ]").
Reserved Notation "A `\` B" (
at level 50, left associativity).
Reserved Notation "A `\ b" (
at level 50, left associativity).
Reserved Notation "\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 < 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 ']'").
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 < 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.
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.
Proof.
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].
Lemma
mksetE
(
P
: T -> Prop)
x
: [set
x
| P x] x = P x.
Proof.
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).
Lemma
subsetP
A
B
: {subset A <= B} <-> (
A `<=` B).
Proof.
by split => + x => /(_ x); rewrite ?inE. Qed.
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 _ _ _ _ /.
Arguments subsetP {T A B}.
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.
Lemma
preimage_itv
T
(
d
: unit) (
rT
: porderType d) (
f
: T -> rT) (
i
: interval rT) (
x
: T)
:
((
f @^-1` [set` i])
x)
= (
f x \in i).
Proof.
Lemma
preimage_itv_o_infty
T
(
d
: unit) (
rT
: porderType d) (
f
: T -> rT)
y
:
f @^-1` `]y, +oo[%classic = [set
x
| (
y < f x)
%O].
Proof.
Lemma
preimage_itv_c_infty
T
(
d
: unit) (
rT
: porderType d) (
f
: T -> rT)
y
:
f @^-1` `[y, +oo[%classic = [set
x
| (
y <= f x)
%O].
Proof.
Lemma
preimage_itv_infty_o
T
(
d
: unit) (
rT
: orderType d) (
f
: T -> rT)
y
:
f @^-1` `]-oo, y[%classic = [set
x
| (
f x < y)
%O].
Proof.
Lemma
preimage_itv_infty_c
T
(
d
: unit) (
rT
: orderType d) (
f
: T -> rT)
y
:
f @^-1` `]-oo, y]%classic = [set
x
| (
f x <= y)
%O].
Proof.
Lemma
eq_set
T
(
P
Q
: T -> Prop)
: (
forall
x
: T, P x = Q x)
->
[set
x
| P x] = [set
x
| Q x].
Proof.
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.
Lemma
set0fun
{P
T
: Type} : @set0 T -> P
Proof.
by case=> x; rewrite inE. Qed.
Lemma
pred_oappE
{T : Type} (
D
: {pred T})
:
pred_oapp D = mem (
some @` D)
%classic.
Proof.
apply/funext=> -[x|]/=; apply/idP/idP; rewrite /pred_oapp/= inE //=.
- by move=> xD; exists x.
- by move=> [// + + [<-]].
- by case.
Qed.
Lemma
pred_oapp_set
{T : Type} (
D
: set T)
:
pred_oapp (
mem D)
= mem (
some @` D)
%classic.
Proof.
by rewrite pred_oappE; apply/funext => x/=; apply/idP/idP; rewrite ?inE;
move=> [y/= ]; rewrite ?in_setE; exists y; rewrite ?in_setE.
Qed.
Section
basic_lemmas
.
Context {T : Type}.
Implicit Types A B C D : set T.
Lemma
mem_set
{A} {u : T} : A u -> u \in A
Proof.
Lemma
set_mem
{A} {u : T} : u \in A -> A u
Proof.
Lemma
mem_setT
(
u
: T)
: u \in [set: T]
Proof.
Lemma
mem_setK
{A} {u : T} : cancel (
@mem_set A u)
set_mem
Proof.
by []. Qed.
Lemma
set_memK
{A} {u : T} : cancel (
@set_mem A u)
mem_set
Proof.
by []. Qed.
Lemma
memNset
(
A
: set T) (
u
: T)
: ~ A u -> u \in A = false.
Proof.
Lemma
notin_set
(
A
: set T)
x
: (
x \notin A : Prop)
= ~ (
A x).
Proof.
by apply/propext; split=> /asboolPn. Qed.
Lemma
setTPn
(
A
: set T)
: A != setT <-> exists
t,
~ A t.
Proof.
#[deprecated(
note="Use setTPn instead")
]
Notation
setTP
:= setTPn (
only parsing).
Lemma
in_set0
(
x
: T)
: (
x \in set0)
= false
Proof.
Lemma
in_setT
(
x
: T)
: x \in setT
Proof.
Lemma
in_setC
(
x
: T)
A
: (
x \in ~` A)
= (
x \notin A).
Proof.
Lemma
in_setI
(
x
: T)
A
B
: (
x \in A `&` B)
= (
x \in A)
&& (
x \in B).
Proof.
by apply/idP/andP; rewrite !inE. Qed.
Lemma
in_setD
(
x
: T)
A
B
: (
x \in A `\` B)
= (
x \in A)
&& (
x \notin B).
Proof.
by apply/idP/andP; rewrite !inE notin_set. Qed.
Lemma
in_setU
(
x
: T)
A
B
: (
x \in A `|` B)
= (
x \in A)
|| (
x \in B).
Proof.
by apply/idP/orP; rewrite !inE. Qed.
Lemma
in_setM
T'
(
x
: T * T')
A
E
: (
x \in A `*` E)
= (
x.
1 \in A)
&& (
x.
2 \in E).
Proof.
by apply/idP/andP; rewrite !inE. Qed.
Lemma
set_valP
{A} (
x
: A)
: A (
val x).
Proof.
Lemma
eqEsubset
A
B
: (
A = B)
= (
A `<=>` B).
Proof.
rewrite propeqE; split => [->|[AB BA]]; [by split|].
by rewrite predeqE => t; split=> [/AB|/BA].
Qed.
Lemma
seteqP
A
B
: (
A = B)
<-> (
A `<=>` B)
Proof.
Lemma
set_true
: [set` predT] = setT :> set T.
Proof.
by apply/seteqP; split. Qed.
Lemma
set_false
: [set` pred0] = set0 :> set T.
Proof.
by apply/seteqP; split. Qed.
Lemma
set_predC
(
P
: {pred T})
: [set` predC P] = ~` [set` P].
Proof.
by apply/seteqP; split => t /negP. Qed.
Lemma
set_andb
(
P
Q
: {pred T})
: [set` predI P Q] = [set` P] `&` [set` Q].
Proof.
by apply/predeqP => x; split; rewrite /= inE => /andP. Qed.
Lemma
set_orb
(
P
Q
: {pred T})
: [set` predU P Q] = [set` P] `|` [set` Q].
Proof.
by apply/predeqP => x; split; rewrite /= inE => /orP. Qed.
Lemma
fun_true
: (
fun=> true)
= setT :> set T.
Proof.
by rewrite [LHS]set_true. Qed.
Lemma
fun_false
: (
fun=> false)
= set0 :> set T.
Proof.
by rewrite [LHS]set_false. Qed.
Lemma
set_mem_set
A
: [set` A] = A.
Proof.
by apply/seteqP; split=> x/=; rewrite inE. Qed.
Lemma
mem_setE
(
P
: pred T)
: mem [set` P] = mem P.
Proof.
by congr Mem; apply/funext=> x; apply/asboolP/idP. Qed.
Lemma
subset_refl
A
: A `<=` A
Proof.
by []. Qed.
Lemma
subset_trans
B
A
C
: A `<=` B -> B `<=` C -> A `<=` C.
Proof.
by move=> sAB sBC ? ?; apply/sBC/sAB. Qed.
Lemma
sub0set
A
: set0 `<=` A
Proof.
by []. Qed.
Lemma
properW
A
B
: A `<` B -> A `<=` B
Proof.
by case. Qed.
Lemma
properxx
A
: ~ A `<` A
Proof.
by move=> [?]; apply. Qed.
Lemma
setC0
: ~` set0 = setT :> set T.
Proof.
Lemma
setCK
: involutive (
@setC T).
Proof.
by move=> A; rewrite funeqE => t; rewrite /setC; exact: notLR. Qed.
Lemma
setCT
: ~` setT = set0 :> set T
Proof.
by rewrite -setC0 setCK. Qed.
Definition
setC_inj
:= can_inj setCK.
Lemma
setIC
: commutative (
@setI T).
Proof.
by move=> A B; rewrite predeqE => ?; split=> [[]|[]]. Qed.
Lemma
setIS
C
A
B
: A `<=` B -> C `&` A `<=` C `&` B.
Proof.
by move=> sAB t [Ct At]; split => //; exact: sAB. Qed.
Lemma
setSI
C
A
B
: A `<=` B -> A `&` C `<=` B `&` C.
Proof.
by move=> sAB; rewrite -!(
setIC C)
; apply setIS. Qed.
Lemma
setISS
A
B
C
D
: A `<=` C -> B `<=` D -> A `&` B `<=` C `&` D.
Proof.
by move=> /(@setSI B) /subset_trans sAC /(@setIS C) /sAC. Qed.
Lemma
setIT
: right_id setT (
@setI T).
Proof.
by move=> A; rewrite predeqE => ?; split=> [[]|]. Qed.
Lemma
setTI
: left_id setT (
@setI T).
Proof.
by move=> A; rewrite predeqE => ?; split=> [[]|]. Qed.
Lemma
setI0
: right_zero set0 (
@setI T).
Proof.
by move=> A; rewrite predeqE => ?; split=> [[]|]. Qed.
Lemma
set0I
: left_zero set0 (
@setI T).
Proof.
Lemma
setICl
: left_inverse set0 setC (
@setI T).
Proof.
by move=> A; rewrite predeqE => ?; split => // -[]. Qed.
Lemma
setICr
: right_inverse set0 setC (
@setI T).
Proof.
Lemma
setIA
: associative (
@setI T).
Proof.
by move=> A B C; rewrite predeqE => ?; split=> [[? []]|[[]]]. Qed.
Lemma
setICA
: left_commutative (
@setI T).
Proof.
by move=> A B C; rewrite setIA [A `&` _]setIC -setIA. Qed.
Lemma
setIAC
: right_commutative (
@setI T).
Proof.
Lemma
setIACA
: @interchange (
set T)
setI setI.
Proof.
by move=> A B C D; rewrite -setIA [B `&` _]setICA setIA. Qed.
Lemma
setIid
: idempotent (
@setI T).
Proof.
by move=> A; rewrite predeqE => ?; split=> [[]|]. Qed.
Lemma
setIIl
A
B
C
: A `&` B `&` C = (
A `&` C)
`&` (
B `&` C).
Proof.
Lemma
setIIr
A
B
C
: A `&` (
B `&` C)
= (
A `&` B)
`&` (
A `&` C).
Proof.
Lemma
setUC
: commutative (
@setU T).
Proof.
move=> p q; rewrite /setU/mkset predeqE => a; tauto. Qed.
Lemma
setUS
C
A
B
: A `<=` B -> C `|` A `<=` C `|` B.
Proof.
by move=> sAB t [Ct|At]; [left|right; exact: sAB]. Qed.
Lemma
setSU
C
A
B
: A `<=` B -> A `|` C `<=` B `|` C.
Proof.
by move=> sAB; rewrite -!(
setUC C)
; apply setUS. Qed.
Lemma
setUSS
A
B
C
D
: A `<=` C -> B `<=` D -> A `|` B `<=` C `|` D.
Proof.
by move=> /(@setSU B) /subset_trans sAC /(@setUS C) /sAC. Qed.
Lemma
setTU
: left_zero setT (
@setU T).
Proof.
by move=> A; rewrite predeqE => t; split; [case|left]. Qed.
Lemma
setUT
: right_zero setT (
@setU T).
Proof.
by move=> A; rewrite predeqE => t; split; [case|right]. Qed.
Lemma
set0U
: left_id set0 (
@setU T).
Proof.
by move=> A; rewrite predeqE => t; split; [case|right]. Qed.
Lemma
setU0
: right_id set0 (
@setU T).
Proof.
by move=> A; rewrite predeqE => t; split; [case|left]. Qed.
Lemma
setUCl
: left_inverse setT setC (
@setU T).
Proof.
move=> A.
by rewrite predeqE => t; split => // _; case: (
pselect (
A t))
; [right|left].
Qed.
Lemma
setUCr
: right_inverse setT setC (
@setU T).
Proof.
Lemma
setUA
: associative (
@setU T).
Proof.
move=> p q r; rewrite /setU/mkset predeqE => a; tauto. Qed.
Lemma
setUCA
: left_commutative (
@setU T).
Proof.
by move=> A B C; rewrite setUA [A `|` _]setUC -setUA. Qed.
Lemma
setUAC
: right_commutative (
@setU T).
Proof.
Lemma
setUACA
: @interchange (
set T)
setU setU.
Proof.
by move=> A B C D; rewrite -setUA [B `|` _]setUCA setUA. Qed.
Lemma
setUid
: idempotent (
@setU T).
Proof.
move=> p; rewrite /setU/mkset predeqE => a; tauto. Qed.
Lemma
setUUl
A
B
C
: A `|` B `|` C = (
A `|` C)
`|` (
B `|` C).
Proof.
Lemma
setUUr
A
B
C
: A `|` (
B `|` C)
= (
A `|` B)
`|` (
A `|` C).
Proof.
Lemma
setU_id2r
C
A
B
:
(
forall
x,
(
~` B)
x -> A x = C x)
-> (
A `|` B)
= (
C `|` B).
Proof.
move=> h; apply/seteqP; split => [x [Ax|Bx]|x [Cx|Bx]]; [|by right| |by right].
- by have [|/h {}h] := pselect (
B x)
; [by right|left; rewrite -h].
- by have [|/h {}h] := pselect (
B x)
; [by right|left; rewrite h].
Qed.
Lemma
setDE
A
B
: A `\` B = A `&` ~` B
Proof.
by []. Qed.
Lemma
setDUK
A
B
: A `<=` B -> A `|` (
B `\` A)
= B.
Proof.
move=> AB; apply/seteqP; split=> [x [/AB//|[//]]|x Bx].
by have [Ax|nAx] := pselect (
A x)
; [left|right].
Qed.
Lemma
setDKU
A
B
: A `<=` B -> (
B `\` A)
`|` A = B.
Proof.
by move=> /setDUK; rewrite setUC. Qed.
Lemma
setDv
A
: A `\` A = set0.
Proof.
by rewrite predeqE => t; split => // -[]. Qed.
Lemma
setUv
A
: A `|` ~` A = setT.
Proof.
by apply/predeqP => x; split=> //= _; apply: lem. Qed.
Lemma
setvU
A
: ~` A `|` A = setT
Proof.
Lemma
setUCK
A
B
: (
A `|` B)
`|` ~` B = setT.
Proof.
Lemma
setUKC
A
B
: ~` A `|` (
A `|` B)
= setT.
Proof.
Lemma
setICK
A
B
: (
A `&` B)
`&` ~` B = set0.
Proof.
Lemma
setIKC
A
B
: ~` A `&` (
A `&` B)
= set0.
Proof.
Lemma
setDIK
A
B
: A `&` (
B `\` A)
= set0.
Proof.
Lemma
setDKI
A
B
: (
B `\` A)
`&` A = set0.
Proof.
Lemma
setD1K
a
A
: A a -> a |` A `\ a = A.
Proof.
by move=> Aa; rewrite setDUK//= => x ->. Qed.
Lemma
setI1
A
a
: A `&` [set a] = if a \in A then [set a] else set0.
Proof.
by apply/predeqP => b; case: ifPn; rewrite (
inE, notin_set)
=> Aa;
split=> [[]|]//; [move=> -> //|move=> /[swap] -> /Aa].
Qed.
Lemma
set1I
A
a
: [set a] `&` A = if a \in A then [set a] else set0.
Proof.
Lemma
subset0
A
: (
A `<=` set0)
= (
A = set0).
Proof.
Lemma
subTset
A
: (
setT `<=` A)
= (
A = setT).
Proof.
Lemma
sub1set
x
A
: (
[set x] `<=` A)
= (
x \in A).
Proof.
by apply/propext; split=> [|/[!inE] xA _ ->//]; rewrite inE; exact. Qed.
Lemma
subsetT
A
: A `<=` setT
Proof.
by []. Qed.
Lemma
subsetW
{A
B}
: A = B -> A `<=` B
Proof.
by move->. Qed.
Definition
subsetCW
{A
B}
: A = B -> B `<=` A := subsetW \o esym.
Lemma
disj_set2E
A
B
: [disjoint A & B] = (
A `&` B == set0).
Proof.
by []. Qed.
Lemma
disj_set2P
{A
B}
: reflect (
A `&` B = set0)
[disjoint A & B]%classic.
Proof.
exact/eqP. Qed.
Lemma
disj_setPS
{A
B}
: reflect (
A `&` B `<=` set0)
[disjoint A & B]%classic.
Proof.
Lemma
disj_set_sym
A
B
: [disjoint B & A] = [disjoint A & B].
Proof.
by rewrite !disj_set2E setIC. Qed.
Lemma
disj_setPCl
{A
B}
: reflect (
A `<=` B)
[disjoint A & ~` B]%classic.
Proof.
Lemma
disj_setPCr
{A
B}
: reflect (
A `<=` B)
[disjoint ~` B & A]%classic.
Proof.
Lemma
disj_setPLR
{A
B}
: reflect (
A `<=` ~` B)
[disjoint A & B]%classic.
Proof.
Lemma
disj_setPRL
{A
B}
: reflect (
B `<=` ~` A)
[disjoint A & B]%classic.
Proof.
Lemma
subsets_disjoint
A
B
: A `<=` B <-> A `&` ~` B = set0.
Proof.
Lemma
disjoints_subset
A
B
: A `&` B = set0 <-> A `<=` ~` B.
Proof.
Lemma
subsetC1
x
A
: (
A `<=` [set~ x])
= (
x \in ~` A).
Proof.
rewrite !inE; apply/propext; split; first by move/[apply]; apply.
by move=> NAx y; apply: contraPnot => ->.
Qed.
Lemma
setSD
C
A
B
: A `<=` B -> A `\` C `<=` B `\` C.
Proof.
by rewrite !setDE; apply: setSI. Qed.
Lemma
setTD
A
: setT `\` A = ~` A.
Proof.
by rewrite predeqE => t; split => // -[]. Qed.
Lemma
set0P
A
: (
A != set0)
<-> (
A !=set0).
Proof.
split=> [/negP A_neq0|[t tA]]; last by apply/negP => /eqP A0; rewrite A0 in tA.
apply: contrapT => /asboolPn/forallp_asboolPn A0; apply/A_neq0/eqP.
by rewrite eqEsubset; split.
Qed.
Lemma
setF_eq0
: (
T -> False)
-> all_equal_to (
set0 : set T).
Proof.
by move=> TF A; rewrite -subset0 => x; have := TF x. Qed.
Lemma
subset_nonempty
A
B
: A `<=` B -> A !=set0 -> B !=set0.
Proof.
by move=> sAB [x Ax]; exists x; apply: sAB. Qed.
Lemma
subsetC
A
B
: A `<=` B -> ~` B `<=` ~` A.
Proof.
by move=> sAB ? nBa ?; apply/nBa/sAB. Qed.
Lemma
subsetCl
A
B
: ~` A `<=` B -> ~` B `<=` A.
Proof.
by move=> /subsetC; rewrite setCK. Qed.
Lemma
subsetCr
A
B
: A `<=` ~` B -> B `<=` ~` A.
Proof.
by move=> /subsetC; rewrite setCK. Qed.
Lemma
subsetC2
A
B
: ~` A `<=` ~` B -> B `<=` A.
Proof.
by move=> /subsetC; rewrite !setCK. Qed.
Lemma
subsetCP
A
B
: ~` A `<=` ~` B <-> B `<=` A.
Proof.
by split=> /subsetC; rewrite ?setCK. Qed.
Lemma
subsetCPl
A
B
: ~` A `<=` B <-> ~` B `<=` A.
Proof.
by split=> /subsetC; rewrite ?setCK. Qed.
Lemma
subsetCPr
A
B
: A `<=` ~` B <-> B `<=` ~` A.
Proof.
by split=> /subsetC; rewrite ?setCK. Qed.
Lemma
subsetUl
A
B
: A `<=` A `|` B
Proof.
by move=> x; left. Qed.
Lemma
subsetUr
A
B
: B `<=` A `|` B
Proof.
by move=> x; right. Qed.
Lemma
subUset
A
B
C
: (
B `|` C `<=` A)
= ((
B `<=` A)
/\ (
C `<=` A)).
Proof.
rewrite propeqE; split => [|[BA CA] x]; last by case; [exact: BA | exact: CA].
by move=> sBC_A; split=> x ?; apply sBC_A; [left | right].
Qed.
Lemma
setIidPl
A
B
: A `&` B = A <-> A `<=` B.
Proof.
rewrite predeqE; split=> [AB t /AB [] //|AB t].
by split=> [[]//|At]; split=> //; exact: AB.
Qed.
Lemma
setIidPr
A
B
: A `&` B = B <-> B `<=` A.
Proof.
Lemma
setIidl
A
B
: A `<=` B -> A `&` B = A
Proof.
Lemma
setIidr
A
B
: B `<=` A -> A `&` B = B
Proof.
Lemma
setUidPl
A
B
: A `|` B = A <-> B `<=` A.
Proof.
split=> [<- ? ?|BA]; first by right.
rewrite predeqE => t; split=> [[//|/BA//]|?]; by left.
Qed.
Lemma
setUidPr
A
B
: A `|` B = B <-> A `<=` B.
Proof.
Lemma
setUidl
A
B
: B `<=` A -> A `|` B = A
Proof.
Lemma
setUidr
A
B
: A `<=` B -> A `|` B = B
Proof.
Lemma
subsetI
A
B
C
: (
A `<=` B `&` C)
= ((
A `<=` B)
/\ (
A `<=` C)).
Proof.
rewrite propeqE; split=> [H|[y z ??]]; split; by [move=> ?/H[]|apply y|apply z].
Qed.
Lemma
setDidPl
A
B
: A `\` B = A <-> A `&` B = set0.
Proof.
Lemma
setDidl
A
B
: A `&` B = set0 -> A `\` B = A.
Proof.
by move=> /setDidPl. Qed.
Lemma
subIset
A
B
C
: A `<=` C \/ B `<=` C -> A `&` B `<=` C.
Proof.
case=> sub a; by [move=> [/sub] | move=> [_ /sub]]. Qed.
Lemma
subIsetl
A
B
: A `&` B `<=` A
Proof.
by move=> x []. Qed.
Lemma
subIsetr
A
B
: A `&` B `<=` B
Proof.
by move=> x []. Qed.
Lemma
subDsetl
A
B
: A `\` B `<=` A.
Proof.
Lemma
subDsetr
A
B
: A `\` B `<=` ~` B.
Proof.
Lemma
subsetI_neq0
A
B
C
D
:
A `<=` B -> C `<=` D -> A `&` C !=set0 -> B `&` D !=set0.
Proof.
by move=> AB CD [x [/AB Bx /CD Dx]]; exists x. Qed.
Lemma
subsetI_eq0
A
B
C
D
:
A `<=` B -> C `<=` D -> B `&` D = set0 -> A `&` C = set0.
Proof.
by move=> AB /(
subsetI_neq0 AB)
; rewrite -!set0P => /contra_eq. Qed.
Lemma
setD_eq0
A
B
: (
A `\` B = set0)
= (
A `<=` B).
Proof.
rewrite propeqE; split=> [ADB0 a|sAB].
by apply: contraPP => nBa xA; rewrite -[False]/(
set0 a)
-ADB0.
by rewrite predeqE => ?; split=> // - [?]; apply; apply: sAB.
Qed.
Lemma
properEneq
A
B
: (
A `<` B)
= (
A != B /\ A `<=` B).
Proof.
Lemma
nonsubset
A
B
: ~ (
A `<=` B)
-> A `&` ~` B !=set0.
Proof.
by rewrite -setD_eq0 setDE -set0P => /eqP. Qed.
Lemma
setU_eq0
A
B
: (
A `|` B = set0)
= ((
A = set0)
/\ (
B = set0)).
Proof.
Lemma
setCS
A
B
: (
~` A `<=` ~` B)
= (
B `<=` A).
Proof.
rewrite propeqE; split => [|BA].
by move/subsets_disjoint; rewrite setCK setIC => /subsets_disjoint.
by apply/subsets_disjoint; rewrite setCK setIC; apply/subsets_disjoint.
Qed.
Lemma
setDT
A
: A `\` setT = set0.
Proof.
Lemma
set0D
A
: set0 `\` A = set0.
Proof.
Lemma
setD0
A
: A `\` set0 = A.
Proof.
Lemma
setDS
C
A
B
: A `<=` B -> C `\` B `<=` C `\` A.
Proof.
by rewrite !setDE -setCS; apply: setIS. Qed.
Lemma
setDSS
A
B
C
D
: A `<=` C -> D `<=` B -> A `\` B `<=` C `\` D.
Proof.
by move=> /(@setSD B) /subset_trans sAC /(@setDS C) /sAC. Qed.
Lemma
setCU
A
B
: ~`(
A `|` B)
= ~` A `&` ~` B.
Proof.
Lemma
setCI
A
B
: ~` (
A `&` B)
= ~` A `|` ~` B.
Proof.
Lemma
setDUr
A
B
C
: A `\` (
B `|` C)
= (
A `\` B)
`&` (
A `\` C).
Proof.
Lemma
setIUl
: left_distributive (
@setI T) (
@setU T).
Proof.
move=> A B C; rewrite predeqE => t; split.
by move=> [[At|Bt] Ct]; [left|right].
by move=> [[At Ct]|[Bt Ct]]; split => //; [left|right].
Qed.
Lemma
setIUr
: right_distributive (
@setI T) (
@setU T).
Proof.
by move=> A B C; rewrite ![A `&` _]setIC setIUl. Qed.
Lemma
setUIl
: left_distributive (
@setU T) (
@setI T).
Proof.
move=> A B C; rewrite predeqE => t; split.
by move=> [[At Bt]|Ct]; split; by [left|right].
by move=> [[At|Ct] [Bt|Ct']]; by [left|right].
Qed.
Lemma
setUIr
: right_distributive (
@setU T) (
@setI T).
Proof.
by move=> A B C; rewrite ![A `|` _]setUC setUIl. Qed.
Lemma
setUK
A
B
: (
A `|` B)
`&` A = A.
Proof.
by rewrite eqEsubset; split => [t []//|t ?]; split => //; left. Qed.
Lemma
setKU
A
B
: A `&` (
B `|` A)
= A.
Proof.
by rewrite eqEsubset; split => [t []//|t ?]; split => //; right. Qed.
Lemma
setIK
A
B
: (
A `&` B)
`|` A = A.
Proof.
by rewrite eqEsubset; split => [t [[]//|//]|t At]; right. Qed.
Lemma
setKI
A
B
: A `|` (
B `&` A)
= A.
Proof.
by rewrite eqEsubset; split => [t [//|[]//]|t At]; left. Qed.
Lemma
setDUl
: left_distributive setD (
@setU T).
Proof.
by move=> A B C; rewrite !setDE setIUl. Qed.
Lemma
setUKD
A
B
: A `&` B `<=` set0 -> (
A `|` B)
`\` A = B.
Proof.
Lemma
setUDK
A
B
: A `&` B `<=` set0 -> (
B `|` A)
`\` A = B.
Proof.
Lemma
setIDA
A
B
C
: A `&` (
B `\` C)
= (
A `&` B)
`\` C.
Proof.
by rewrite !setDE setIA. Qed.
Lemma
setDD
A
B
: A `\` (
A `\` B)
= A `&` B.
Proof.
Lemma
setDDl
A
B
C
: (
A `\` B)
`\` C = A `\` (
B `|` C).
Proof.
Lemma
setDDr
A
B
C
: A `\` (
B `\` C)
= (
A `\` B)
`|` (
A `&` C).
Proof.
Lemma
setDIr
A
B
C
: A `\` B `&` C = (
A `\` B)
`|` (
A `\` C).
Proof.
Lemma
setUIDK
A
B
: (
A `&` B)
`|` A `\` B = A.
Proof.
Lemma
setM0
T'
(
A
: set T)
: A `*` set0 = set0 :> set (
T * T').
Proof.
by rewrite predeqE => -[t u]; split => // -[]. Qed.
Lemma
set0M
T'
(
A
: set T')
: set0 `*` A = set0 :> set (
T * T').
Proof.
by rewrite predeqE => -[t u]; split => // -[]. Qed.
Lemma
setMTT
T'
: setT `*` setT = setT :> set (
T * T').
Proof.
exact/predeqP. Qed.
Lemma
setMT
T1
T2
(
A
: set T1)
: A `*` @setT T2 = fst @^-1` A.
Proof.
by rewrite predeqE => -[x y]; split => //= -[]. Qed.
Lemma
setTM
T1
T2
(
B
: set T2)
: @setT T1 `*` B = snd @^-1` B.
Proof.
by rewrite predeqE => -[x y]; split => //= -[]. Qed.
Lemma
setMI
T1
T2
(
X1
: set T1) (
X2
: set T2) (
Y1
: set T1) (
Y2
: set T2)
:
(
X1 `&` Y1)
`*` (
X2 `&` Y2)
= X1 `*` X2 `&` Y1 `*` Y2.
Proof.
by rewrite predeqE => -[x y]; split=> [[[? ?] [*]//]|[] [? ?] [*]]. Qed.
Lemma
setSM
T1
T2
(
C
D
: set T1) (
A
B
: set T2)
:
A `<=` B -> C `<=` D -> C `*` A `<=` D `*` B.
Proof.
by move=> AB CD x [] /CD Dx1 /AB Bx2. Qed.
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).
Proof.
rewrite predeqE => -[x y]; split; first by move=> [/= Ax [n Pn Fny]]; exists n.
by move=> [n Pn [/= Ax Fny]]; split => //; exists n.
Qed.
Lemma
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).
Proof.
rewrite predeqE => -[x y]; split; first by move=> [[n Pn Fnx] Ax]; exists n.
by move=> [n Pn [/= Ax Fny]]; split => //; exists n.
Qed.
Lemma
bigcupM1l
T1
T2
(
A1
: set T1) (
A2
: T1 -> set T2)
:
\bigcup_(
i
in A1) (
[set i] `*` (
A2 i))
= A1 `*`` A2.
Proof.
by apply/predeqP => -[i j]; split=> [[? ? [/= -> //]]|[]]; exists i. Qed.
Lemma
bigcupM1r
T1
T2
(
A1
: T2 -> set T1) (
A2
: set T2)
:
\bigcup_(
i
in A2) (
A1 i `*` [set i])
= A1 ``*` A2.
Proof.
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 (
only parsing).
#[deprecated(
since="mathcomp-analysis 0.6", note="Use setICr instead.")
]
Notation
setIv
:= setICr (
only parsing).
Arguments setU_id2r {T} C {A B}.
Section
set_order
.
Import Order.TTheory.
Lemma
set_eq_le
d
(
rT
: porderType d)
T
(
f
g
: T -> rT)
:
[set
x
| f x = g x] = [set
x
| (
f x <= g x)
%O] `&` [set
x
| (
f x >= g x)
%O].
Proof.
by apply/seteqP; split => [x/= ->//|x /andP]; rewrite -eq_le =>/eqP. Qed.
Lemma
set_neq_lt
d
(
rT
: orderType d)
T
(
f
g
: T -> rT)
:
[set
x
| f x != g x ] = [set
x
| (
f x < g x)
%O] `|` [set
x
| (
f x > g x)
%O].
Proof.
by apply/seteqP; split => [x/=|x /=]; rewrite neq_lt => /orP. Qed.
End set_order.
Lemma
image2E
{TA
TB
rT
: Type} (
A
: set TA) (
B
: set TB) (
f
: TA -> TB -> rT)
:
[set f x y |
x
in A &
y
in B] = uncurry f @` (
A `*` B).
Proof.
apply/predeqP => x; split=> [[a ? [b ? <-]]|[[a b] [? ? <-]]]/=;
by [exists (a, b) | exists a => //; exists b].
Qed.
Lemma
set_nil
(
T
: eqType)
: [set` [::]] = @set0 T.
Proof.
Lemma
set_cons1
(
T
: eqType) (
x
: T)
: [set` [:: x]] = [set x].
Proof.
by apply/seteqP; split => y /=; rewrite ?inE => /eqP. Qed.
Lemma
set_seq_eq0
(
T
: eqType) (
S
: seq T)
: (
[set` S] == set0)
= (
S == [::]).
Proof.
apply/eqP/eqP=> [|->]; rewrite predeqE //; case: S => // h t /(
_ h).
by rewrite /= mem_head => -[/(
_ erefl)
].
Qed.
Lemma
set_fset_eq0
(
T
: choiceType) (
S
: {fset T})
:
(
[set` S] == set0)
= (
S == fset0).
Proof.
Section
InitialSegment
.
Lemma
II0
: `I_0 = set0
Proof.
Lemma
II1
: `I_1 = [set 0]
Proof.
Lemma
IIn_eq0
n
: `I_n = set0 -> n = 0.
Proof.
by case: n => // n; rewrite predeqE; case/(
_ 0%N)
; case. Qed.
Lemma
IIS
n
: `I_n.
+1 = `I_n `|` [set n].
Proof.
rewrite /mkset predeqE => i; split => [|[|->//]].
by rewrite ltnS leq_eqVlt => /orP[/eqP ->|]; by [left|right].
by move/ltn_trans; apply.
Qed.
Lemma
IISl
n
: `I_n.
+1 = n |` `I_n.
Proof.
Lemma
IIDn
n
: `I_n.
+1 `\ n = `I_n.
Proof.
Lemma
setI_II
m
n
: `I_m `&` `I_n = `I_(
minn m n).
Proof.
Lemma
setU_II
m
n
: `I_m `|` `I_n = `I_(
maxn m n).
Proof.
Lemma
Iiota
(
n
: nat)
: [set` iota 0 n] = `I_n.
Proof.
Definition
ordII
{n} (
k
: 'I_n)
: `I_n := SigSub (
@mem_set _ `I_n _ (
ltn_ord k)).
Definition
IIord
{n} (
k
: `I_n)
:= Ordinal (
set_valP k).
Definition
ordIIK
{n} : cancel (
@ordII n)
IIord.
Proof.
by move=> k; apply/val_inj. Qed.
Lemma
IIordK
{n} : cancel (
@IIord n)
ordII.
Proof.
by move=> k; apply/val_inj. Qed.
Lemma
mem_not_I
N
n
: (
n \in ~` `I_N)
= (
N <= n).
Proof.
by rewrite in_setC /mkset /in_mem /mem /= /in_set asboolb -leqNgt. Qed.
End InitialSegment.
Lemma
setT_unit
: [set: unit] = [set tt].
Proof.
by apply/seteqP; split => // -[]. Qed.
Lemma
set_unit
(
A
: set unit)
: A = set0 \/ A = setT.
Proof.
have [->|/set0P[[] Att]] := eqVneq A set0; [by left|right].
by apply/seteqP; split => [|] [].
Qed.
Lemma
setT_bool
: [set: bool] = [set true; false].
Proof.
by rewrite eqEsubset; split => // [[]] // _; [left|right]. Qed.
Lemma
set_bool
(
B
: set bool)
:
[\/ B == [set true], B == [set false], B == set0 | B == setT].
Proof.
have [Bt|Bt] := boolP (
true \in B)
; have [Bf|Bf] := boolP (
false \in B).
- have -> : B = setT by apply/seteqP; split => // -[] _; exact: set_mem.
by apply/or4P; rewrite eqxx/= !orbT.
- suff : B = [set true] by move=> ->; apply/or4P; rewrite eqxx.
apply/seteqP; split => -[]// /mem_set; last by move=> _; exact: set_mem.
by rewrite (
negbTE Bf).
- suff : B = [set false] by move=> ->; apply/or4P; rewrite eqxx/= orbT.
apply/seteqP; split => -[]// /mem_set; last by move=> _; exact: set_mem.
by rewrite (
negbTE Bt).
- suff : B = set0 by move=> ->; apply/or4P; rewrite eqxx/= !orbT.
by apply/seteqP; split => -[]//=; rewrite 2!notin_set in Bt, Bf.
Qed.
Lemma
fdisjoint_cset
(
T
: choiceType) (
A
B
: {fset T})
:
[disjoint A & B]%fset = [disjoint [set` A] & [set` B]].
Proof.
rewrite -fsetI_eq0; apply/idP/idP; apply: contraLR.
by move=> /set0P[t [tA tB]]; apply/fset0Pn; exists t; rewrite inE; apply/andP.
by move=> /fset0Pn[t]; rewrite inE => /andP[tA tB]; apply/set0P; exists t.
Qed.
Section
SetFset
.
Context {T : choiceType}.
Implicit Types (
x y : T) (
A B : {fset T}).
Lemma
set_fset0
: [set
y
: T | y \in fset0] = set0.
Proof.
by rewrite -subset0 => x. Qed.
Lemma
set_fset1
x
: [set
y
| y \in [fset x]%fset] = [set x].
Proof.
by rewrite predeqE => y; split; rewrite /= inE => /eqP. Qed.
Lemma
set_fsetI
A
B
: [set` (
A `&` B)
%fset] = [set` A] `&` [set` B].
Proof.
by rewrite predeqE => x; split; rewrite /= !inE; [case/andP|case=> -> ->].
Qed.
Lemma
set_fsetIr
(
P
: {pred T}) (
A
: {fset T})
:
[set` [fset x |
x
in A & P x]%fset] = [set` A] `&` [set` P].
Proof.
by apply/predeqP => x /=; split; rewrite 2!inE/= => /andP. Qed.
Lemma
set_fsetU
A
B
:
[set` (
A `|` B)
%fset] = [set` A] `|` [set` B].
Proof.
rewrite predeqE => x; split; rewrite /= !inE.
by case/orP; [left|right].
by move=> []->; rewrite ?orbT.
Qed.
Lemma
set_fsetU1
x
A
: [set
y
| y \in (
x |` A)
%fset] = x |` [set` A].
Proof.
Lemma
set_fsetD
A
B
:
[set` (
A `\` B)
%fset] = [set` A] `\` [set` B].
Proof.
rewrite predeqE => x; split; rewrite /= !inE; last by move=> [-> /negP ->].
by case/andP => /negP xNB xA.
Qed.
Lemma
set_fsetD1
A
x
: [set
y
| y \in (
A `\ x)
%fset] = [set` A] `\ x.
Proof.
Lemma
set_imfset
(
key
: unit)
[K : choiceType] (
f
: T -> K) (
p
: finmempred T)
:
[set` imfset key f p] = f @` [set` p].
Proof.
apply/predeqP => x; split=> [/imfsetP[i ip -> /=]|]; first by exists i.
by move=> [i ip <-]; apply: in_imfset.
Qed.
End SetFset.
Section
SetMonoids
.
Variable (
T
: Type).
Import Monoid.
Canonical
setU_monoid
:= Law (
@setUA T) (
@set0U T) (
@setU0 T).
Canonical
setU_comoid
:= ComLaw (
@setUC T).
Canonical
setU_mul_monoid
:= MulLaw (
@setTU T) (
@setUT T).
Canonical
setI_monoid
:= Law (
@setIA T) (
@setTI T) (
@setIT T).
Canonical
setI_comoid
:= ComLaw (
@setIC T).
Canonical
setI_mul_monoid
:= MulLaw (
@set0I T) (
@setI0 T).
Canonical
setU_add_monoid
:= AddLaw (
@setUIl T) (
@setUIr T).
Canonical
setI_add_monoid
:= AddLaw (
@setIUl T) (
@setIUr T).
End SetMonoids.
Section
base_image_lemmas
.
Context {aT
rT
: Type}.
Implicit Types (
A B : set aT) (
f : aT -> rT) (
Y : set rT).
Lemma
imageP
f
A
a
: A a -> (
f @` A) (
f a)
Proof.
by exists a. Qed.
Lemma
imageT
(
f
: aT -> rT) (
a
: aT)
: range f (
f a).
Proof.
End base_image_lemmas.
#[global]
Hint Extern 0 ((
?f @` _) (
?f _))
=> solve [apply: imageP; assumption] : core.
#[global] Hint Extern 0 ((
?f @` setT)
_)
=> solve [apply: imageT] : core.
Section
image_lemmas
.
Context {aT
rT
: Type}.
Implicit Types (
A B : set aT) (
f : aT -> rT) (
Y : set rT).
Lemma
image_inj
{f
A
a}
: injective f -> (
f @` A) (
f a)
= A a.
Proof.
by move=> f_inj; rewrite propeqE; split => [[b Ab /f_inj <-]|/(
imageP f)
//].
Qed.
Lemma
image_id
A
: id @` A = A.
Proof.
by rewrite eqEsubset; split => a; [case=> /= x Ax <-|exists a]. Qed.
Lemma
homo_setP
{A
Y
f}
:
{homo f :
x
/ x \in A >-> x \in Y} <-> {homo f :
x
/ A x >-> Y x}.
Proof.
by split=> fAY x; have := fAY x; rewrite !inE. Qed.
Lemma
image_subP
{A
Y
f}
: f @` A `<=` Y <-> {homo f :
x
/ A x >-> Y x}.
Proof.
by split=> fAY x => [Ax|[y + <-]]; apply: fAY=> //; exists x. Qed.
Lemma
image_sub
{f : aT -> rT} {A : set aT} {B : set rT} :
(
f @` A `<=` B)
= (
A `<=` f @^-1` B).
Proof.
by apply/propext; rewrite image_subP; split=> AB a /AB. Qed.
Lemma
imsub1
x
A
f
: f @` A `<=` [set x] -> forall
a,
A a -> f a = x.
Proof.
by move=> + a Aa; apply; exists a. Qed.
Lemma
imsub1P
x
A
f
: f @` A `<=` [set x] <-> forall
a,
A a -> f a = x.
Proof.
by split=> [/(@imsub1 _)//|+ _ [a Aa <-]]; apply. Qed.
Lemma
image_setU
f
A
B
: f @` (
A `|` B)
= f @` A `|` f @` B.
Proof.
rewrite eqEsubset; split => b.
- by case=> a [] Ha <-; [left | right]; apply imageP.
- by case=> -[] a Ha <-; apply imageP; [left | right].
Qed.
Lemma
image_set0
f
: f @` set0 = set0.
Proof.
Lemma
image_set0_set0
A
f
: f @` A = set0 -> A = set0.
Proof.
move=> fA0; rewrite predeqE => t; split => // At.
by have : set0 (
f t)
by rewrite -fA0; exists t.
Qed.
Lemma
image_set1
f
t
: f @` [set t] = [set f t].
Proof.
by rewrite eqEsubset; split => [b [a' -> <-] //|b ->]; exact/imageP. Qed.
Lemma
subset_set1
A
a
: A `<=` [set a] -> A = set0 \/ A = [set a].
Proof.
move=> Aa; have [/eqP|/set0P[t At]] := boolP (
A == set0)
; first by left.
by right; rewrite eqEsubset; split => // ? ->; rewrite -(
Aa _ At).
Qed.
Lemma
subset_set2
A
a
b
: A `<=` [set a; b] ->
[\/ A = set0, A = [set a], A = [set b] | A = [set a; b]].
Proof.
Lemma
sub_image_setI
f
A
B
: f @` (
A `&` B)
`<=` f @` A `&` f @` B.
Proof.
by move=> b [x [Aa Ba <-]]; split; apply: imageP. Qed.
Lemma
nonempty_image
f
A
: f @` A !=set0 -> A !=set0.
Proof.
by case=> b [a]; exists a. Qed.
Lemma
image_subset
f
A
B
: A `<=` B -> f @` A `<=` f @` B.
Proof.
by move=> AB _ [a Aa <-]; exists a => //; apply/AB. Qed.
Lemma
preimage_set0
f
: f @^-1` set0 = set0
Proof.
exact/predeqP. Qed.
Lemma
preimage_setT
f
: f @^-1` setT = setT
Proof.
by []. Qed.
Lemma
nonempty_preimage
f
Y
: f @^-1` Y !=set0 -> Y !=set0.
Proof.
by case=> [t ?]; exists (f t). Qed.
Lemma
preimage_image
f
A
: A `<=` f @^-1` (
f @` A).
Proof.
by move=> a Aa; exists a. Qed.
Lemma
preimage_range
{A
B
: Type} (
f
: A -> B)
: f @^-1` (
range f)
= [set: A].
Proof.
by rewrite eqEsubset; split=> x // _; exists x. Qed.
Lemma
image_preimage_subset
f
Y
: f @` (
f @^-1` Y)
`<=` Y.
Proof.
by move=> _ [t /= Yft <-]. Qed.
Lemma
image_preimage
f
Y
: f @` setT = setT -> f @` (
f @^-1` Y)
= Y.
Proof.
move=> fsurj; rewrite predeqE => x; split; first by move=> [? ? <-].
move=> Yx; have : setT x by [].
by rewrite -fsurj => - [y _ fy_eqx]; exists y => //=; rewrite fy_eqx.
Qed.
Lemma
eq_imagel
T1
T2
(
A
: set T1) (
f
f'
: T1 -> T2)
:
(
forall
x,
A x -> f x = f' x)
-> f @` A = f' @` A.
Proof.
by move=> h; rewrite predeqE=> y; split=> [][x ? <-]; exists x=> //; rewrite h.
Qed.
Lemma
eq_image_id
g
A
: (
forall
x,
A x -> g x = x)
-> g @` A = A.
Proof.
by move=> /eq_imagel->; rewrite image_id. Qed.
Lemma
preimage_setU
f
Y1
Y2
: f @^-1` (
Y1 `|` Y2)
= f @^-1` Y1 `|` f @^-1` Y2.
Proof.
exact/predeqP. Qed.
Lemma
preimage_setI
f
Y1
Y2
: f @^-1` (
Y1 `&` Y2)
= f @^-1` Y1 `&` f @^-1` Y2.
Proof.
exact/predeqP. Qed.
Lemma
preimage_setC
f
Y
: ~` (
f @^-1` Y)
= f @^-1` (
~` Y).
Proof.
by rewrite predeqE => a; split=> nAfa ?; apply: nAfa. Qed.
Lemma
preimage_subset
f
Y1
Y2
: Y1 `<=` Y2 -> f @^-1` Y1 `<=` f @^-1` Y2.
Proof.
by move=> Y12 t /Y12. Qed.
Lemma
nonempty_preimage_setI
f
Y1
Y2
:
(
f @^-1` (
Y1 `&` Y2))
!=set0 <-> (
f @^-1` Y1 `&` f @^-1` Y2)
!=set0.
Proof.
by split; case=> t ?; exists t. Qed.
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).
Proof.
exact/predeqP. Qed.
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).
Proof.
exact/predeqP. Qed.
Lemma
eq_preimage
{I
T
: Type} (
D
: set I) (
A
: set T) (
F
G
: I -> T)
:
{in D, F =1 G} -> D `&` F @^-1` A = D `&` G @^-1` A.
Proof.
move=> eqFG; apply/predeqP => i.
by split=> [] [Di FAi]; split; rewrite /preimage//= (eqFG,=^~eqFG) ?inE.
Qed.
Lemma
notin_setI_preimage
T
R
D
(
f
: T -> R)
i
:
i \notin f @` D -> D `&` f @^-1` [set i] = set0.
Proof.
Lemma
comp_preimage
T1
T2
T3
(
A
: set T3) (
g
: T1 -> T2) (
f
: T2 -> T3)
:
(
f \o g)
@^-1` A = g @^-1` (
f @^-1` A).
Proof.
by []. Qed.
Lemma
preimage_id
T
(
A
: set T)
: id @^-1` A = A
Proof.
by []. Qed.
Lemma
preimage_comp
T1
T2
(
g
: T1 -> rT) (
f
: T2 -> rT) (
C
: set T1)
:
f @^-1` [set g x |
x
in C] = [set
x
| f x \in g @` C].
Proof.
rewrite predeqE => t; split => /=.
by move=> -[r Cr <-]; rewrite inE; exists r.
by rewrite inE => -[r Cr <-]; exists r.
Qed.
Lemma
preimage_setI_eq0
(
f
: aT -> rT) (
Y1
Y2
: set rT)
:
f @^-1` (
Y1 `&` Y2)
= set0 <-> f @^-1` Y1 `&` f @^-1` Y2 = set0.
Proof.
Lemma
preimage0eq
(
f
: aT -> rT) (
Y
: set rT)
: Y = set0 -> f @^-1` Y = set0.
Proof.
Lemma
preimage0
{T
R}
{f : T -> R} {A : set R} :
A `&` range f `<=` set0 -> f @^-1` A = set0.
Proof.
by rewrite -subset0 => + x /= Afx => /(_ (f x))[]; split. Qed.
Lemma
preimage10P
{T
R}
{f : T -> R} {x} : ~ range f x <-> f @^-1` [set x] = set0.
Proof.
split => [fx|]; first by rewrite preimage0// => ? [->].
by apply: contraPnot => -[t _ <-] /seteqP[+ _] => /(
_ t)
/=.
Qed.
Lemma
preimage10
{T
R}
{f : T -> R} {x} : ~ range f x -> f @^-1` [set x] = set0.
Proof.
by move/preimage10P. Qed.
Lemma
preimage_true
{T} (
P
: {pred T})
: P @^-1` [set true] = [set` P].
Proof.
by apply/seteqP; split => [x/=//|x]. Qed.
Lemma
preimage_false
{T} (
P
: {pred T})
: P @^-1` [set false] = ~` [set` P].
Proof.
by apply/seteqP; split => [t/= /negbT/negP|t /= /negP/negbTE]. Qed.
Lemma
preimage_mem_true
{T} (
A
: set T)
: mem A @^-1` [set true] = A.
Proof.
Lemma
preimage_mem_false
{T} (
A
: set T)
: mem A @^-1` [set false] = ~` A.
Proof.
End image_lemmas.
Arguments sub_image_setI {aT rT f A B} t _.
Lemma
image2_subset
{aT
bT
rT
: Type} (
f
: aT -> bT -> rT)
(
A
B
: set aT) (
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].
Proof.
Lemma
image_comp
T1
T2
T3
(
f
: T1 -> T2) (
g
: T2 -> T3)
A
:
g @` (
f @` A)
= (
g \o f)
@` A.
Proof.
by rewrite eqEsubset; split => [x [b [a Aa] <- <-]|x [a Aa] <-];
[apply/imageP |apply/imageP/imageP].
Qed.
Lemma
subKimage
{T
T'}
{P : set (
set T')
} (
f
: T -> T') (
g
: T' -> T)
:
cancel f g -> [set
A
| P (
f @` A)
] `<=` [set g @` A |
A
in P].
Proof.
by move=> ? A; exists (f @` A); rewrite ?image_comp ?eq_image_id/=. Qed.
Lemma
subimageK
T
T'
(
P
: set (
set T')) (
f
: T -> T') (
g
: T' -> T)
:
cancel g f -> [set g @` A |
A
in P] `<=` [set
A
| P (
f @` A)
].
Proof.
Lemma
eq_imageK
{T
T'}
{P : set (
set T')
} (
f
: T -> T') (
g
: T' -> T)
:
cancel f g -> cancel g f ->
[set g @` A |
A
in P] = [set
A
| P (
f @` A)
].
Proof.
Lemma
some_set0
{T} : some @` set0 = set0 :> set (
option T).
Proof.
by rewrite -subset0 => x []. Qed.
Lemma
some_set1
{T} (
x
: T)
: some @` [set x] = [set some x].
Proof.
by apply/seteqP; split=> [_ [_ -> <-]|_ ->]//=; exists x. Qed.
Lemma
some_setC
{T} (
A
: set T)
: some @` (
~` A)
= [set~ None] `\` (
some @` A).
Proof.
apply/seteqP; split; first by move=> _ [x nAx <-]; split=> // -[y /[swap]-[->]].
by move=> [x [_ exAx]|[/(
_ erefl)
//]]; exists x => // Ax; apply: exAx; exists x.
Qed.
Lemma
some_setT
{T} : some @` [set: T] = [set~ None].
Proof.
Lemma
some_setI
{T} (
A
B
: set T)
: some @` (
A `&` B)
= some @` A `&` some @` B.
Proof.
apply/seteqP; split; first by move=> _ [x [Ax Bx] <-]; split; exists x.
by move=> _ [[x + <-] [y By []]] => /[swap]<- Ay; exists y.
Qed.
Lemma
some_setU
{T} (
A
B
: set T)
: some @` (
A `|` B)
= some @` A `|` some @` B.
Proof.
Lemma
some_setD
{T} (
A
B
: set T)
: some @` (
A `\` B)
= (
some @` A)
`\` (
some @` B).
Proof.
Lemma
sub_image_some
{T} (
A
B
: set T)
: some @` A `<=` some @` B -> A `<=` B.
Proof.
by move=> + x Ax => /(
_ (
Some x))
[|y By [<-]]; first by exists x. Qed.
Lemma
sub_image_someP
{T} (
A
B
: set T)
: some @` A `<=` some @` B <-> A `<=` B.
Proof.
by split=> [/sub_image_some//|/image_subset]. Qed.
Lemma
image_some_inj
{T} (
A
B
: set T)
: some @` A = some @` B -> A = B.
Proof.
Lemma
some_set_eq0
{T} (
A
: set T)
: some @` A = set0 <-> A = set0.
Proof.
split=> [|->]; last by rewrite some_set0.
by rewrite -!subset0 => A0 x Ax; apply: (
A0 (
some x))
; exists x.
Qed.
Lemma
some_preimage
{aT
rT}
(
f
: aT -> rT) (
A
: set rT)
:
some @` (
f @^-1` A)
= omap f @^-1` (
some @` A).
Proof.
apply/seteqP; split; first by move=> _ [a Afa <-]; exists (f a).
by move=> [x|] [a Aa //= [afx]]; exists x; rewrite // -afx.
Qed.
Lemma
some_image
{aT
rT}
(
f
: aT -> rT) (
A
: set aT)
:
some @` (
f @` A)
= omap f @` (
some @` A).
Proof.
by rewrite !image_comp. Qed.
Lemma
disj_set_some
{T} {A
B
: set T} :
[disjoint some @` A & some @` B] = [disjoint A & B].
Proof.
by apply/disj_setPS/disj_setPS; rewrite -some_setI -some_set0 sub_image_someP.
Qed.
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.
Proof.
by move=> Pi a Fia; exists i. Qed.
Lemma
bigcap_inf
i
P
F
: P i -> \bigcap_(
j
in P)
F j `<=` F i.
Proof.
by move=> Pi a /(_ i); apply. Qed.
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}.
Proof.
move=> F G FG t [i Pi Fit]; have := FG (
F i).
by move=> /(
_ (
ex_intro2 _ _ _ Pi erefl))
[j Pj ji]; exists j => //; rewrite ji.
Qed.
Lemma
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}.
Proof.
by move=> F G FG t Gt i Pi; have [|j Pj <-] := FG (
F i)
; [exists i|apply: Gt].
Qed.
Lemma
eq_bigcupr
P
F
G
: (
forall
i,
P i -> F i = G i)
->
\bigcup_(
i
in P)
F i = \bigcup_(
i
in P)
G i.
Proof.
Lemma
eq_bigcapr
P
F
G
: (
forall
i,
P i -> F i = G i)
->
\bigcap_(
i
in P)
F i = \bigcap_(
i
in P)
G i.
Proof.
Lemma
setC_bigcup
P
F
: ~` (
\bigcup_(
i
in P)
F i)
= \bigcap_(
i
in P)
~` F i.
Proof.
by rewrite eqEsubset; split => [t PFt i Pi ?|t PFt [i Pi ?]];
[apply PFt; exists i | exact: (
PFt _ Pi)
].
Qed.
Lemma
setC_bigcap
P
F
: ~` (
\bigcap_(
i
in P) (
F i))
= \bigcup_(
i
in P)
~` F i.
Proof.
Lemma
image_bigcup
rT
P
F
(
f
: T -> rT)
:
f @` (
\bigcup_(
i
in P) (
F i))
= \bigcup_(
i
in P)
f @` F i.
Proof.
apply/seteqP; split=> [_/= [x [i Pi Fix <-]]|]; first by exists i.
by move=> _ [i Pi [x Fix <-]]; exists x => //; exists i.
Qed.
Lemma
some_bigcap
P
F
: some @` (
\bigcap_(
i
in P) (
F i))
=
[set~ None] `&` \bigcap_(
i
in P)
some @` F i.
Proof.
apply/seteqP; split.
by move=> _ [x Fx <-]; split=> // i; exists x => //; apply: Fx.
by move=> [x|[//=]] [_ Fx]; exists x => //= i /Fx [y ? [<-]].
Qed.
Lemma
bigcup_set_type
P
F
: \bigcup_(
i
in P)
F i = \bigcup_(
j
: P)
F (
val j).
Proof.
rewrite predeqE => x; split; last by move=> [[i/= /set_mem Pi] _ Fix]; exists i.
by move=> [i Pi Fix]; exists (
SigSub (
mem_set Pi)).
Qed.
Lemma
eq_bigcupl
P
Q
F
: P `<=>` Q ->
\bigcup_(
i
in P)
F i = \bigcup_(
i
in Q)
F i.
Proof.
by move=> /seteqP->. Qed.
Lemma
eq_bigcapl
P
Q
F
: P `<=>` Q ->
\bigcap_(
i
in P)
F i = \bigcap_(
i
in Q)
F i.
Proof.
by move=> /seteqP->. Qed.
Lemma
eq_bigcup
P
Q
F
G
: P `<=>` Q -> (
forall
i,
P i -> F i = G i)
->
\bigcup_(
i
in P)
F i = \bigcup_(
i
in Q)
G i.
Proof.
by move=> /eq_bigcupl<- /eq_bigcupr->. Qed.
Lemma
eq_bigcap
P
Q
F
G
: P `<=>` Q -> (
forall
i,
P i -> F i = G i)
->
\bigcap_(
i
in P)
F i = \bigcap_(
i
in Q)
G i.
Proof.
by move=> /eq_bigcapl<- /eq_bigcapr->. Qed.
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).
Proof.
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.
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).
Proof.
Lemma
bigcup_const
P
A
: P !=set0 -> \bigcup_(
_ in P)
A = A.
Proof.
by case=> j ?; rewrite predeqE => x; split=> [[i //]|Ax]; exists j. Qed.
Lemma
bigcap_const
P
A
: P !=set0 -> \bigcap_(
_ in P)
A = A.
Proof.
Lemma
bigcapIl
P
F
A
: P !=set0 ->
\bigcap_(
i
in P) (
F i `&` A)
= \bigcap_(
i
in P)
F i `&` A.
Proof.
Lemma
bigcapIr
P
F
A
: P !=set0 ->
\bigcap_(
i
in P) (
A `&` F i)
= A `&` \bigcap_(
i
in P)
F i.
Proof.
Lemma
bigcupUl
P
F
A
: P !=set0 ->
\bigcup_(
i
in P) (
F i `|` A)
= \bigcup_(
i
in P)
F i `|` A.
Proof.
Lemma
bigcupUr
P
F
A
: P !=set0 ->
\bigcup_(
i
in P) (
A `|` F i)
= A `|` \bigcup_(
i
in P)
F i.
Proof.
Lemma
bigcup_set0
F
: \bigcup_(
i
in set0)
F i = set0.
Proof.
Lemma
bigcup_set1
F
i
: \bigcup_(
j
in [set i])
F j = F i.
Proof.
by rewrite eqEsubset; split => ? => [[] ? -> //|]; exists i. Qed.
Lemma
bigcap_set0
F
: \bigcap_(
i
in set0)
F i = setT.
Proof.
Lemma
bigcap_set1
F
i
: \bigcap_(
j
in [set i])
F j = F i.
Proof.
by rewrite eqEsubset; split => ?; [exact|move=> ? ? ->]. Qed.
Lemma
bigcup_nonempty
P
F
:
(
\bigcup_(
i
in P)
F i !=set0)
<-> exists2
i,
P i & F i !=set0.
Proof.
split=> [[t [i ? ?]]|[j ? [t ?]]]; by [exists i => //; exists t| exists t, j].
Qed.
Lemma
bigcup0
P
F
:
(
forall
i,
P i -> F i = set0)
-> \bigcup_(
i
in P)
F i = set0.
Proof.
by move=> PF; rewrite -subset0 => t -[i /PF ->]. Qed.
Lemma
bigcap0
P
F
:
(
exists2
i,
P i & F i = set0)
-> \bigcap_(
i
in P)
F i = set0.
Proof.
by move=> [i Pi]; rewrite -!subset0 => Fi t Ft; apply/Fi/Ft. Qed.
Lemma
bigcapT
P
F
:
(
forall
i,
P i -> F i = setT)
-> \bigcap_(
i
in P)
F i = setT.
Proof.
by move=> PF; rewrite -subTset => t -[i /PF ->]. Qed.
Lemma
bigcupT
P
F
:
(
exists2
i,
P i & F i = setT)
-> \bigcup_(
i
in P)
F i = setT.
Proof.
by move=> [i Pi F0]; rewrite -subTset => t; exists i; rewrite ?F0. Qed.
Lemma
bigcup0P
P
F
:
(
\bigcup_(
i
in P)
F i = set0)
<-> forall
i,
P i -> F i = set0.
Proof.
split=> [|/bigcup0//]; rewrite -subset0 => F0 i Pi; rewrite -subset0.
by move=> t Ft; apply: F0; exists i.
Qed.
Lemma
bigcapTP
P
F
:
(
\bigcap_(
i
in P)
F i = setT)
<-> forall
i,
P i -> F i = setT.
Proof.
split=> [|/bigcapT//]; rewrite -subTset => FT i Pi; rewrite -subTset.
by move=> t _; apply: FT.
Qed.
Lemma
setI_bigcupr
F
P
A
:
A `&` \bigcup_(
i
in P)
F i = \bigcup_(
i
in P) (
A `&` F i).
Proof.
rewrite predeqE => t; split => [[At [k ? ?]]|[k ? [At ?]]];
by [exists k |split => //; exists k].
Qed.
Lemma
setI_bigcupl
F
P
A
:
\bigcup_(
i
in P)
F i `&` A = \bigcup_(
i
in P) (
F i `&` A).
Proof.
Lemma
setU_bigcapr
F
P
A
:
A `|` \bigcap_(
i
in P)
F i = \bigcap_(
i
in P) (
A `|` F i).
Proof.
Lemma
setU_bigcapl
F
P
A
:
\bigcap_(
i
in P)
F i `|` A = \bigcap_(
i
in P) (
F i `|` A).
Proof.
Lemma
bigcup_mkcond
P
F
:
\bigcup_(
i
in P)
F i = \bigcup_i if i \in P then F i else set0.
Proof.
Lemma
bigcup_mkcondr
P
Q
F
:
\bigcup_(
i
in P `&` Q)
F i = \bigcup_(
i
in P)
if i \in Q then F i else set0.
Proof.
Lemma
bigcup_mkcondl
P
Q
F
:
\bigcup_(
i
in P `&` Q)
F i = \bigcup_(
i
in Q)
if i \in P then F i else set0.
Proof.
Lemma
bigcap_mkcond
F
P
:
\bigcap_(
i
in P)
F i = \bigcap_i if i \in P then F i else setT.
Proof.
Lemma
bigcap_mkcondr
P
Q
F
:
\bigcap_(
i
in P `&` Q)
F i = \bigcap_(
i
in P)
if i \in Q then F i else setT.
Proof.
Lemma
bigcap_mkcondl
P
Q
F
:
\bigcap_(
i
in P `&` Q)
F i = \bigcap_(
i
in Q)
if i \in P then F i else setT.
Proof.
Lemma
bigcup_imset1
P
(
f
: I -> T)
: \bigcup_(
x
in P)
[set f x] = f @` P.
Proof.
by rewrite eqEsubset; split=>[a [i ?]->| a [i ?]<-]; [apply: imageP | exists i].
Qed.
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.
Proof.
rewrite predeqE => t; split=> [[z]|].
by move=> [Xz|Yz]; [left|right]; exists z.
by move=> [[z Xz Fzy]|[z Yz Fxz]]; exists z => //; [left|right].
Qed.
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.
Proof.
Lemma
bigcup_setU1
F
(
x
: I) (
X
: set I)
:
\bigcup_(
i
in x |` X)
F i = F x `|` \bigcup_(
i
in X)
F i.
Proof.
Lemma
bigcap_setU1
F
(
x
: I) (
X
: set I)
:
\bigcap_(
i
in x |` X)
F i = F x `&` \bigcap_(
i
in X)
F i.
Proof.
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.
Proof.
by move=> Xx; rewrite -bigcup_setU1 setD1K. Qed.
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.
Proof.
by move=> Xx; rewrite -bigcap_setU1 setD1K. Qed.
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.
Proof.
by elim/big_rec2: _ => [|i X Y Pi <-]; rewrite ?setC0 ?setCU. Qed.
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.
Proof.
by elim/big_rec2: _ => [|i X Y Pi <-]; rewrite ?setCT ?setCI. Qed.
Lemma
bigcupDr
(
F
: I -> set T) (
P
: set I) (
A
: set T)
: P !=set0 ->
\bigcap_(
i
in P) (
A `\` F i)
= A `\` \bigcup_(
i
in P)
F i.
Proof.
Lemma
setD_bigcupl
(
F
: I -> set T) (
P
: set I) (
A
: set T)
:
\bigcup_(
i
in P)
F i `\` A = \bigcup_(
i
in P) (
F i `\` A).
Proof.
Lemma
bigcup_setM_dep
{J : Type} (
F
: I -> J -> set T)
(
P
: set I) (
Q
: I -> set J)
:
\bigcup_(
k
in P `*`` Q)
F k.
1 k.
2 = \bigcup_(
i
in P)
\bigcup_(
j
in Q i)
F i j.
Proof.
apply/predeqP => x; split=> [|[i Pi [j Pj Fijx]]]; last by exists (i, j).
by move=> [[/= i j] [Pi Qj] Fijx]; exists i => //; exists j.
Qed.
Lemma
bigcup_setM
{J : Type} (
F
: I -> J -> set T) (
P
: set I) (
Q
: set J)
:
\bigcup_(
k
in P `*` Q)
F k.
1 k.
2 = \bigcup_(
i
in P)
\bigcup_(
j
in Q)
F i j.
Proof.
Lemma
bigcup_bigcup
T'
(
F
: I -> set T) (
P
: set I) (
G
: T -> set T')
:
\bigcup_(
i
in \bigcup_(
n
in P)
F n)
G i =
\bigcup_(
n
in P)
\bigcup_(
i
in F n)
G i.
Proof.
apply/seteqP; split; first by move=> x [n [m ? ?] h]; exists m => //; exists n.
by move=> x [n ? [m ?]] h; exists m => //; exists n.
Qed.
Lemma
bigcupID
(
Q
: set I) (
F
: I -> set T) (
P
: set I)
:
\bigcup_(
i
in P)
F i =
(
\bigcup_(
i
in P `&` Q)
F i)
`|` (
\bigcup_(
i
in P `&` ~` Q)
F i).
Proof.
Lemma
bigcapID
(
Q
: set I) (
F
: I -> set T) (
P
: set I)
:
\bigcap_(
i
in P)
F i =
(
\bigcap_(
i
in P `&` Q)
F i)
`&` (
\bigcap_(
i
in P `&` ~` Q)
F i).
Proof.
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 /.
Lemma
bigcup2E
T
(
A
B
: set T)
: \bigcup_i (
bigcup2 A B)
i = A `|` B.
Proof.
rewrite predeqE => t; split=> [|[At|Bt]]; [|by exists 0|by exists 1].
by case=> -[_ At|[_ Bt|//]]; [left|right].
Qed.
Lemma
bigcup2inE
T
(
A
B
: set T)
: \bigcup_(
i
< 2) (
bigcup2 A B)
i = A `|` B.
Proof.
rewrite predeqE => t; split=> [|[At|Bt]]; [|by exists 0|by exists 1].
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 /.
Lemma
bigcap2E
T
(
A
B
: set T)
: \bigcap_i (
bigcap2 A B)
i = A `&` B.
Proof.
Lemma
bigcap2inE
T
(
A
B
: set T)
: \bigcap_(
i
< 2) (
bigcap2 A B)
i = A `&` B.
Proof.
Lemma
bigcup_sub
T
I
(
F
: I -> set T) (
D
: set T) (
P
: set I)
:
(
forall
i,
P i -> F i `<=` D)
-> \bigcup_(
i
in P)
F i `<=` D.
Proof.
by move=> FD t [n Pn Fnt]; apply: (FD n). Qed.
Lemma
sub_bigcap
T
I
(
F
: I -> set T) (
D
: set T) (
P
: set I)
:
(
forall
i,
P i -> D `<=` F i)
-> D `<=` \bigcap_(
i
in P)
F i.
Proof.
by move=> DF t Dt n Pn; apply: DF. Qed.
Lemma
subset_bigcup
T
I
[P : set I] [F
G
: I -> set T] :
(
forall
i,
P i -> F i `<=` G i)
->
\bigcup_(
i
in P)
F i `<=` \bigcup_(
i
in P)
G i.
Proof.
Lemma
subset_bigcap
T
I
[P : set I] [F
G
: I -> set T] :
(
forall
i,
P i -> F i `<=` G i)
->
\bigcap_(
i
in P)
F i `<=` \bigcap_(
i
in P)
G i.
Proof.
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).
Proof.
rewrite eqEsubset; split=> x; first by case=> j [] i pi <- Xfix; exists i.
by case=> i Pi Ffix; exists (
f i)
; [exists i|].
Qed.
Lemma
bigcap_set_type
{I
T}
(
P
: set I) (
F
: I -> set T)
:
\bigcap_(
i
in P)
F i = \bigcap_(
j
: P)
F (
val j).
Proof.
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).
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
Arguments bigcup_fsetD1 {T U} x.
Section
bigcup_seq
.
Variables (
T
: choiceType) (
U
: Type).
Lemma
bigcup_seq_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).
Proof.
elim: s => [/=|h s ih]; first by rewrite set_nil bigcup_set0 big_nil.
rewrite big_cons -ih predeqE => u; split=> [[t /andP[]]|].
- rewrite inE => /orP[/eqP ->{t} -> fhu|ts Pt ftu]; first by left.
case: ifPn => Ph; first by right; exists t => //; apply/andP; split.
by exists t => //; apply/andP; split.
- case: ifPn => [Ph [fhu|[t /andP[ts Pt] ftu]]|Ph [t /andP[ts Pt ftu]]].
+ by exists h => //; apply/andP; split => //; rewrite mem_head.
+ by exists t => //; apply/andP; split => //; rewrite inE orbC ts.
+ by exists t => //; apply/andP; split => //; rewrite inE orbC ts.
Qed.
Lemma
bigcup_seq
(
s
: seq T) (
f
: T -> set U)
:
\bigcup_(
t
in [set` s]) (
f t)
= \big[setU/set0]_(
t
<- s) (
f t).
Proof.
Lemma
bigcap_seq_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).
Proof.
Lemma
bigcap_seq
(
s
: seq T) (
f
: T -> set U)
:
\bigcap_(
t
in [set` s]) (
f t)
= \big[setI/setT]_(
t
<- s) (
f t).
Proof.
End bigcup_seq.
#[deprecated(
since="mathcomp-analysis 0.6.4",note="Use bigcup_seq instead")
]
Notation
bigcup_set
:= bigcup_seq (
only parsing).
#[deprecated(
since="mathcomp-analysis 0.6.4",note="Use bigcup_seq_cond instead")
]
Notation
bigcup_set_cond
:= bigcup_seq_cond (
only parsing).
#[deprecated(
since="mathcomp-analysis 0.6.4",note="Use bigcap_seq instead")
]
Notation
bigcap_set
:= bigcap_seq (
only parsing).
#[deprecated(
since="mathcomp-analysis 0.6.4",note="Use bigcap_seq_cond instead")
]
Notation
bigcap_set_cond
:= bigcap_seq_cond (
only parsing).
Lemma
bigcup_pred
[T : finType] [U : Type] (
P
: {pred T}) (
f
: T -> set U)
:
\bigcup_(
t
in [set` P])
f t = \big[setU/set0]_(
t
in P)
f t.
Proof.
apply/predeqP => u; split=> [[x Px fxu]|]; first by rewrite (
bigD1 x)
//; left.
move=> /mem_set; rewrite (
@big_morph _ _ (
fun
X
=> u \in X)
false orb).
- by rewrite big_has_cond => /hasP[x _ /andP[xP]]; rewrite inE => ufx; exists x.
- by move=> /= x y; apply/idP/orP; rewrite !inE.
- 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.
Lemma
sub_smallest
X
: X `<=` G -> X `<=` smallest.
Proof.
by move=> XG A /XG GA Y /= [PY]; apply. Qed.
Lemma
sub_gen_smallest
: G `<=` smallest
Proof.
Lemma
smallest_sub
X
: C X -> G `<=` X -> smallest `<=` X.
Proof.
by move=> XC GX A; apply. Qed.
Lemma
smallest_id
: C G -> smallest = G.
Proof.
End smallest.
#[global] Hint Resolve sub_gen_smallest : core.
Lemma
sub_smallest2r
{T} (
C
: set T-> Prop)
G1
G2
:
C (
smallest C G2)
-> G1 `<=` G2 -> smallest C G1 `<=` smallest C G2.
Proof.
Lemma
sub_smallest2l
{T} (
C1
C2
: set T -> Prop)
:
(
forall
G,
C2 G -> C1 G)
->
forall
G,
smallest C1 G `<=` smallest C2 G.
Proof.
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).
Lemma
bigcup_mkord
n
F
: \bigcup_(
i
< n)
F i = \big[setU/set0]_(
i
< n)
F i.
Proof.
Lemma
bigcap_mkord
n
F
: \bigcap_(
i
< n)
F i = \big[setI/setT]_(
i
< n)
F i.
Proof.
Lemma
bigsetU_sup
i
n
F
: (
i < n)
%N -> F i `<=` \big[setU/set0]_(
j
< n)
F j.
Proof.
by move: n => // n ni; rewrite -bigcup_mkord; exact/bigcup_sup. Qed.
Lemma
bigsetU_bigcup
F
n
: \big[setU/set0]_(
i
< n)
F i `<=` \bigcup_k F k.
Proof.
by rewrite -bigcup_mkord => x [k _ Fkx]; exists k. Qed.
Lemma
bigsetU_bigcup2
(
A
B
: set T)
:
\big[setU/set0]_(
i
< 2)
bigcup2 A B i = A `|` B.
Proof.
Lemma
bigsetI_bigcap2
(
A
B
: set T)
:
\big[setI/setT]_(
i
< 2)
bigcap2 A B i = A `&` B.
Proof.
Lemma
bigcup_splitn
n
F
:
\bigcup_i F i = \big[setU/set0]_(
i
< n)
F i `|` \bigcup_i F (
n + i).
Proof.
rewrite -bigcup_mkord -(
bigcup_image _ (
addn n))
-bigcup_setU.
apply: eq_bigcupl; split=> // k _.
have [ltkn|lenk] := ltnP k n; [left => //|right].
by exists (
k - n)
; rewrite // subnKC.
Qed.
Lemma
bigcap_splitn
n
F
:
\bigcap_i F i = \big[setI/setT]_(
i
< n)
F i `&` \bigcap_i F (
n + i).
Proof.
Lemma
subset_bigsetU
F
:
{homo (
fun
n
=> \big[setU/set0]_(
i
< n)
F i)
:
n
m
/ (
n <= m)
>-> n `<=` m}.
Proof.
move=> m n mn; rewrite -!bigcup_mkord => x [i im Fix].
by exists i => //=; rewrite (
leq_trans im).
Qed.
Lemma
subset_bigsetI
F
:
{homo (
fun
n
=> \big[setI/setT]_(
i
< n)
F i)
:
n
m
/ (
n <= m)
>-> m `<=` n}.
Proof.
move=> m n mn; rewrite -setCS !setC_bigsetI.
exact: (
@subset_bigsetU (
setC \o F)).
Qed.
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 `<=` m}.
Proof.
Lemma
subset_bigsetI_cond
(
P
: pred nat)
F
:
{homo (
fun
n
=> \big[setI/setT]_(
i
< n | P i)
F i)
:
n
m
/ (
n <= m)
>-> m `<=` n}.
Proof.
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.
Lemma
xgetP
{T : choiceType}
x0
(
P
: set T)
:
xget_spec x0 P (
xget x0 P) (
P (
xget x0 P)).
Proof.
move: (
erefl (
xget x0 P))
; set y := {2}(
xget x0 P).
rewrite /xget; case: pselect => /= [?|neqP _].
by case: sigW => x /= /asboolP Px; rewrite [P x]propT //; constructor.
suff NP x : ~ P x by rewrite [P x0]propF //; constructor.
by apply: contra_not neqP => Px; exists x; apply/asboolP.
Qed.
Lemma
xgetPex
{T : choiceType}
x0
(
P
: set T)
: (
exists
x,
P x)
-> P (
xget x0 P).
Proof.
by case: xgetP=> // NP [x /NP]. Qed.
Lemma
xgetI
{T : choiceType}
x0
(
P
: set T) (
x
: T)
: P x -> P (
xget x0 P).
Proof.
by move=> Px; apply: xgetPex; exists x. Qed.
Lemma
xget_subset1
{T : choiceType}
x0
(
P
: set T) (
x
: T)
:
P x -> is_subset1 P -> xget x0 P = x.
Proof.
by move=> Px /(
_ _ _ (
xgetI x0 Px)
Px). Qed.
Lemma
xget_unique
{T : choiceType}
x0
(
P
: set T) (
x
: T)
:
P x -> (
forall
y,
P y -> y = x)
-> xget x0 P = x.
Proof.
by move=> /xget_subset1 gPx eqx; apply: gPx=> y z /eqx-> /eqx. Qed.
Lemma
xgetPN
{T : choiceType}
x0
(
P
: set T)
:
(
forall
x,
~ P x)
-> xget x0 P = x0.
Proof.
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).
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).
Proof.
by move=> [b fab]; rewrite /fun_of_rel; apply: xgetI fab. Qed.
Lemma
fun_of_rel_uniq
{aT} {rT : choiceType}
(
f
: aT -> rT -> Prop) (
f0
: aT -> rT)
a
:
is_subset1 (
f a)
-> forall
b,
f a b -> fun_of_rel f0 f a = b.
Proof.
by move=> fa1 b /xget_subset1 xgeteq; rewrite /fun_of_rel xgeteq. Qed.
Lemma
forall_sig
T
(
A
: set T) (
P
: {x | x \in A} -> Prop)
:
(
forall
u
: {x | x \in A}, P u)
=
(
forall
u
: T, forall (
a
: A u)
, P (
exist _ u (
mem_set a))).
Proof.
Lemma
in_setP
{U} (
A
: set U) (
P
: U -> Prop)
:
{in A, forall
x,
P x} <-> forall
x,
A x -> P x.
Proof.
by split=> AP x; have := AP x; rewrite inE. Qed.
Lemma
in_set2P
{U
V}
(
A
: set U) (
B
: set V) (
P
: U -> V -> Prop)
:
{in A & B, forall
x
y,
P x y} <-> (
forall
x
y,
A x -> B y -> P x y).
Proof.
by split=> AP x y; have := AP x y; rewrite !inE. Qed.
Lemma
in1TT
[T1] [P1 : T1 -> Prop] :
{in [set: T1], forall
x
: T1, P1 x : Prop} -> forall
x
: T1, P1 x : Prop.
Proof.
by move=> + *; apply; rewrite !inE. Qed.
Lemma
in2TT
[T1
T2]
[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.
Proof.
by move=> + *; apply; rewrite !inE. Qed.
Lemma
in3TT
[T1
T2
T3]
[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.
Proof.
by move=> + *; apply; rewrite !inE. Qed.
Lemma
inTT_bij
[T1
T2
: Type] [f : T1 -> T2] :
{in [set: T1], bijective f} -> bijective f.
Proof.
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.
Notation
"[ 'get' x : T | E ]"
:= (
get (
fun
x
: T => E))
(
at level 0, x name, format "[ 'get' x : T | E ]", only parsing)
: form_scope.
Notation
"[ 'get' x | E ]"
:= (
get (
fun
x
=> E))
(
at level 0, x name, format "[ 'get' x | E ]")
: form_scope.
Section
PointedTheory
.
Context {T : pointedType}.
Lemma
getPex
(
P
: set T)
: (
exists
x,
P x)
-> P (
get P).
Proof.
Lemma
getI
(
P
: set T) (
x
: T)
: P x -> P (
get P).
Proof.
Lemma
get_subset1
(
P
: set T) (
x
: T)
: P x -> is_subset1 P -> get P = x.
Proof.
Lemma
get_unique
(
P
: set T) (
x
: T)
:
P x -> (
forall
y,
P y -> y = x)
-> get P = x.
Proof.
Lemma
getPN
(
P
: set T)
: (
forall
x,
~ P x)
-> get P = point.
Proof.
Lemma
setT0
: setT != set0 :> set T.
Proof.
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)).
Lemma
unsquashK
{T} : cancel (
@unsquash T)
squash
Proof.
by move=> []. Qed.
Module
Empty
.
Definition
mixin_of
T
:= T -> False.
Section
EqMixin
.
Variables (
T
: Type) (
m
: mixin_of T).
Definition
eq_op
(
x
y
: T)
:= true.
Lemma
eq_opP
: Equality.axiom eq_op
Proof.
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.
Lemma
findP
(
P
: pred T) (
n
: nat) (
x
: T)
: find P n = Some x -> P x.
Proof.
by []. Qed.
Lemma
ex_find
(
P
: pred T)
: (
exists
x
: T, P x)
-> exists
n
: nat, find P n.
Proof.
by case. Qed.
Lemma
eq_find
(
P
Q
: pred T)
: P =1 Q -> find P =1 find Q.
Proof.
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.
Lemma
pickleK
: pcancel pickle unpickle
Proof.
by []. Qed.
Definition
countMixin
:= CountMixin pickleK.
End CountMixin.
Section
FinMixin
.
Variables (
T
: countType) (
m
: mixin_of T).
Lemma
fin_axiom
: Finite.axiom (
[::] : seq T)
Proof.
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.
Coercion eqMixin : mixin_of >-> Equality.mixin_of.
Coercion choiceMixin : mixin_of >-> Choice.mixin_of.
Coercion countMixin : mixin_of >-> Countable.mixin_of.
End Exports.
End Empty.
Export Empty.Exports.
Definition
False_emptyMixin
: Empty.mixin_of False := id.
Canonical
False_eqType
:= EqType False False_emptyMixin.
Canonical
False_choiceType
:= ChoiceType False False_emptyMixin.
Canonical
False_countType
:= CountType False False_emptyMixin.
Canonical
False_finType
:= FinType False (
Empty.finMixin False_emptyMixin).
Canonical
False_emptyType
:= EmptyType False False_emptyMixin.
Definition
void_emptyMixin
: Empty.mixin_of void := @of_void _.
Canonical
void_emptyType
:= EmptyType void void_emptyMixin.
Definition
no
{T : emptyType} : T -> False :=
let: Empty.Pack _ (
Empty.Class _ f)
:= T in f.
Definition
any
{T : emptyType} {U} : T -> U := @False_rect _ \o no.
Lemma
empty_eq0
{T : emptyType} : all_equal_to (
set0 : set T).
Proof.
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).
Lemma
qcanon
T
C
(
sort
: C -> T) (
alt
: emptyType -> T)
:
(
forall
x,
(
exists
y
: emptyType, alt y = x)
+ (
exists
y,
sort y = x))
->
quasi_canonical_ sort alt.
Proof.
by move=> + G Cx Gs x => /(_ x)[/cid[y <-]|/cid[y <-]]. Qed.
Arguments qcanon {T C sort alt} x.
Lemma
choicePpointed
: quasi_canonical choiceType pointedType.
Proof.
Lemma
eqPpointed
: quasi_canonical eqType pointedType.
Proof.
by apply: qcanon; elim/eqPchoice; elim/choicePpointed => [[T F]|T];
[left; exists (
Empty.Pack F)
| right; exists T].
Qed.
Lemma
Ppointed
: quasi_canonical Type pointedType.
Proof.
by apply: qcanon; elim/Peq; elim/eqPpointed => [[T F]|T];
[left; exists (
Empty.Pack F)
| right; exists T].
Qed.
Section
partitions
.
Definition
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.
Lemma
trivIset1
T
I
(
i
: I) (
F
: I -> set T)
: trivIset [set i] F.
Proof.
by move=> j k <- <-. Qed.
Lemma
ltn_trivIset
T
(
F
: nat -> set T)
:
(
forall
n
m,
(
m < n)
%N -> F m `&` F n = set0)
-> trivIset setT F.
Proof.
move=> h m n _ _ [t [mt nt]]; apply/eqP/negPn/negP.
by rewrite neq_ltn => /orP[] /h; apply/eqP/set0P; exists t.
Qed.
Lemma
subsetC_trivIset
T
(
F
: nat -> set T)
:
(
forall
n,
F n.
+1 `<=` ~` \big[setU/set0]_(
i
< n.
+1)
F i)
-> trivIset setT F.
Proof.
move=> sF; apply: ltn_trivIset => n m h; rewrite setIC; apply/disjoints_subset.
by case: n h => // n h; apply: (
subset_trans (
sF n))
; exact/subsetC/bigsetU_sup.
Qed.
Lemma
trivIset_mkcond
T
I
(
D
: set I) (
F
: I -> set T)
:
trivIset D F <-> trivIset setT (
fun
i
=> if i \in D then F i else set0).
Proof.
Lemma
trivIset_set0
{I
T}
(
D
: set I)
: trivIset D (
fun=> set0 : set T).
Proof.
by move=> i j Di Dj; rewrite setI0 => /set0P; rewrite eqxx. Qed.
Lemma
trivIsetP
{T} {I : eqType} {D : set I} {F : I -> set T} :
trivIset D F <->
forall
i
j
: I, D i -> D j -> i != j -> F i `&` F j = set0.
Proof.
split=> tDF i j Di Dj; first by apply: contraNeq => /set0P/tDF->.
by move=> /set0P; apply: contraNeq => /tDF->.
Qed.
Lemma
trivIset_bigsetUI
T
(
D
: {pred nat}) (
F
: nat -> set T)
: trivIset D F ->
forall
n
m,
D m -> n <= m -> \big[setU/set0]_(
i
< n | D i)
F i `&` F m = set0.
Proof.
Lemma
trivIset_setIl
(
T
I
: Type) (
D
: set I) (
F
: I -> set T) (
G
: I -> set T)
:
trivIset D F -> trivIset D (
fun
i
=> G i `&` F i).
Proof.
by move=> tF i j Di Dj [x [[Gix Fix] [Gjx Fjx]]]; apply tF => //; exists x.
Qed.
Lemma
trivIset_setIr
(
T
I
: Type) (
D
: set I) (
F
: I -> set T) (
G
: I -> set T)
:
trivIset D F -> trivIset D (
fun
i
=> F i `&` G i).
Proof.
by move=> tF i j Di Dj [x [[Fix Gix] [Fjx Gjx]]]; apply tF => //; exists x.
Qed.
Lemma
sub_trivIset
I
T
(
D
D'
: set I) (
F
: I -> set T)
:
D `<=` D' -> trivIset D' F -> trivIset D F.
Proof.
by move=> DD' Ftriv i j /DD' + /DD' + /Ftriv->//. Qed.
Lemma
trivIset_bigcup2
T
(
A
B
: set T)
:
(
A `&` B = set0)
= trivIset setT (
bigcup2 A B).
Proof.
apply/propext; split=> [AB0|/trivIsetP/(
_ 0 1 Logic.I Logic.I erefl)
//].
apply/trivIsetP => -[/=|]; rewrite /bigcup2 /=.
- by move=> [//|[_ _ _ //|j _ _ _]]; rewrite setI0.
- move=> [[j _ _|]|i j _ _ _]; [by rewrite setIC| |by rewrite set0I].
by move=> [//|j _ _ _]; rewrite setI0.
Qed.
Lemma
trivIset_image
T
I
I'
(
D
: set I) (
f
: I -> I') (
F
: I' -> set T)
:
trivIset D (
F \o f)
-> trivIset (
f @` D)
F.
Proof.
by move=> trivF i j [{}i Di <-] [{}j Dj <-] Ffij; congr (f _); apply: trivF.
Qed.
Arguments trivIset_image {T I I'} D f F.
Lemma
trivIset_comp
T
I
I'
(
D
: set I) (
f
: I -> I') (
F
: I' -> set T)
:
{in D &, injective f} ->
trivIset D (
F \o f)
= trivIset (
f @` D)
F.
Proof.
move=> finj; apply/propext; split; first exact: trivIset_image.
move=> trivF i j Di Dj Ffij; apply: finj; rewrite ?in_setE//.
by apply: trivF => //=; [exists i| exists j].
Qed.
Lemma
trivIset_preimage1
{aT
rT}
D
(
f
: aT -> rT)
:
trivIset D (
fun
x
=> f @^-1` [set x]).
Proof.
by move=> y z _ _ [x [<- <-]]. Qed.
Lemma
trivIset_preimage1_in
{aT} {rT : choiceType} (
D
: set rT) (
A
: set aT)
(
f
: aT -> rT)
: trivIset D (
fun
x
=> A `&` f @^-1` [set x]).
Proof.
by move=> y z _ _ [x [[_ <-] [_ <-]]]. Qed.
Lemma
trivIset_bigcup
(
I
T
: Type) (
J
: eqType) (
D
: J -> set I) (
F
: I -> set T)
:
(
forall
n,
trivIset (
D n)
F)
->
(
forall
n
m
i
j,
n != m -> D n i -> D m j -> F i `&` F j !=set0 -> i = j)
->
trivIset (
\bigcup_k D k)
F.
Proof.
move=> tB H; move=> i j [n _ Dni] [m _ Dmi] ij.
have [nm|nm] := eqVneq n m; first by apply: (
tB m)
=> //; rewrite -nm.
exact: (
H _ _ _ _ nm).
Qed.
Lemma
trivIsetT_bigcup
T1
T2
(
I
: eqType) (
D
: I -> set T1) (
F
: T1 -> set T2)
:
trivIset setT D ->
trivIset (
\bigcup_i D i)
F ->
trivIset setT (
fun
i
=> \bigcup_(
t
in D i)
F t).
Proof.
move=> D0 h i j _ _ [t [[m Dim Fmt] [n Djn Fnt]]].
have mn : m = n by apply: h => //; [exists i|exists j|exists t].
rewrite {}mn {m} in Dim Fmt *.
by apply: D0 => //; exists n.
Qed.
Definition
cover
T
I
D
(
F
: I -> set T)
:= \bigcup_(
i
in D)
F i.
Lemma
coverE
T
I
D
(
F
: I -> set T)
: cover D F = \bigcup_(
i
in D)
F i.
Proof.
by []. Qed.
Lemma
cover_restr
T
I
D'
D
(
F
: I -> set T)
:
D `<=` D' -> (
forall
i,
D' i -> ~ D i -> F i = set0)
->
cover D F = cover D' F.
Proof.
move=> DD' D'DF; rewrite /cover eqEsubset; split=> [r [i Di Fit]|r [i D'i Fit]].
- by have [D'i|] := pselect (
D' i)
; [exists i | have := DD' _ Di].
- by have [Di|Di] := pselect (
D i)
; [exists i | move: Fit; rewrite (
D'DF i)
].
Qed.
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.
Proof.
move=> FG.
rewrite eqEsubset; split => [t [i Di Fit]|t [i Di Git]].
have [j Dj GF] : [set G i |
i
in D] (
F i)
by rewrite -FG /mkset; exists i.
by exists j => //; rewrite GF.
have [j Dj GF] : [set F i |
i
in D] (
G i)
by rewrite FG /mkset; exists i.
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).
Notation
trivIsets
X := (
trivIset X id).
Lemma
trivIset_sets
T
I
D
(
F
: I -> set T)
:
trivIset D F -> trivIsets [set F i |
i
in D].
Proof.
Lemma
trivIset_widen
T
I
D'
D
(
F
: I -> set T)
:
D `<=` D' -> (
forall
i,
D' i -> ~ D i -> F i = set0)
->
trivIset D F = trivIset D' F.
Proof.
move=> DD' DD'F.
rewrite propeqE; split=> [DF i j D'i D'j FiFj0|D'F i j Di Dj FiFj0].
have [Di|Di] := pselect (
D i)
; last first.
by move: FiFj0; rewrite (
DD'F i)
// set0I => /set0P; rewrite eqxx.
have [Dj|Dj] := pselect (
D j).
- exact: DF.
- by move: FiFj0; rewrite (
DD'F j)
// setI0 => /set0P; rewrite eqxx.
by apply D'F => //; apply DD'.
Qed.
Lemma
perm_eq_trivIset
{T : eqType} (
s1
s2
: seq (
set T)) (
D
: set nat)
:
[set
k
| (
k < size s1)
] `<=` D -> perm_eq s1 s2 ->
trivIset D (
fun
i
=> nth set0 s1 i)
-> trivIset D (
fun
i
=> nth set0 s2 i).
Proof.
End partitions.
#[deprecated(
note="Use trivIset_setIl instead")
]
Notation
trivIset_setI
:= trivIset_setIl (
only parsing).
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).
Lemma
ZL'
: False.
Proof.
have lub_ub (
A
: {A : set T | total_on A R})
:
forall
s,
sval A s -> R s (
lub A).
suff /getPex [] : exists
t
: Tp, (
forall
s,
sval A s -> R s t)
/\
forall
r,
(
forall
s,
sval A s -> R s r)
-> R t r by [].
by apply: tot_lub; apply: (
svalP A).
have lub_lub (
A
: {A : set T | total_on A R})
:
forall
t,
(
forall
s,
sval A s -> R s t)
-> R (
lub A)
t.
suff /getPex [] : exists
t
: Tp, (
forall
s,
sval A s -> R s t)
/\
forall
r,
(
forall
s,
sval A s -> R s r)
-> R t r by [].
by apply: tot_lub; apply: (
svalP A).
have RS s : R s (
succ s)
/\ s <> succ s.
by have /getPex [? []] : exists
t
: Tp, R s t /\ s <> t /\
forall
r,
R s r -> R r t -> r = s \/ r = t by apply: Rsucc.
have succS s : forall
t,
R s t -> R t (
succ s)
-> t = s \/ t = succ s.
by have /getPex [? []] : exists
t
: Tp, R s t /\ s <> t /\
forall
r,
R s r -> R r t -> r = s \/ r = t by apply: Rsucc.
suff Twtot : total_on tower R.
have [R_S] := RS (
lub (
exist _ tower Twtot))
; apply.
by apply/Rantisym => //; apply/lub_ub/Succ/Lub.
move=> s t Tws; elim: Tws t => {s} [A sATw ihA|s Tws ihs] t Twt.
have [?|/asboolP] := pselect (
forall
s,
sval A s -> R s t).
by left; apply: lub_lub.
rewrite asbool_neg => /existsp_asboolPn [s /asboolP].
rewrite asbool_neg => /imply_asboolPn [As nRst]; right.
by have /lub_ub := As; apply: Rtrans; have [] := ihA _ As _ Twt.
suff /(
_ _ Twt)
[Rts|RSst] : forall
r,
tower r -> R r s \/ R (
succ s)
r.
by right; apply: Rtrans Rts _; have [] := RS s.
by left.
move=> r; elim=> {r} [A sATw ihA|r Twr ihr].
have [?|/asboolP] := pselect (
forall
r,
sval A r -> R r s).
by left; apply: lub_lub.
rewrite asbool_neg => /existsp_asboolPn [r /asboolP].
rewrite asbool_neg => /imply_asboolPn [Ar nRrs]; right.
by have /lub_ub := Ar; apply: Rtrans; have /ihA [] := Ar.
have [Rrs|RSsr] := ihr; last by right; apply: Rtrans RSsr _; have [] := RS r.
have : tower (
succ r)
by apply: Succ.
move=> /ihs [RsSr|]; last by left.
by have [->|->] := succS _ _ Rrs RsSr; [right|left]; apply: Rrefl.
Qed.
End ZL.
Lemma
Zorn
T
(
R
: T -> T -> Prop)
:
(
forall
t,
R t t)
-> (
forall
r
s
t,
R r s -> R s t -> R r t)
->
(
forall
s
t,
R s t -> R t s -> s = t)
->
(
forall
A
: set T, total_on A R -> exists
t,
forall
s,
A s -> R s t)
->
exists
t,
forall
s,
R t s -> s = t.
Proof.
move=> Rrefl Rtrans Rantisym Rtot_max.
pose totR := {A : set T | total_on A R}.
set R' := fun
A
B
: totR => sval A `<=` sval B.
have R'refl A : R' A A by [].
have R'trans A B C : R' A B -> R' B C -> R' A C by apply: subset_trans.
have R'antisym A B : R' A B -> R' B A -> A = B.
rewrite /R'; move: A B => [/= A totA] [/= B totB] sAB sBA.
by apply: eq_exist; rewrite predeqE=> ?; split=> [/sAB|/sBA].
have R'tot_lub A : 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.
move=> Atot.
have AUtot : total_on (
\bigcup_(
B
in A) (
sval B))
R.
move=> s t [B AB Bs] [C AC Ct].
have [/(
_ _ Bs)
Cs|/(
_ _ Ct)
Bt] := Atot _ _ AB AC.
by have /(
_ _ _ Cs Ct)
:= svalP C.
by have /(
_ _ _ Bs Bt)
:= svalP B.
exists (
exist _ (
\bigcup_(
B
in A)
sval B)
AUtot)
; split.
by move=> B ? ? ?; exists B.
by move=> B Bub ? /= [? /Bub]; apply.
apply: contrapT => nomax.
have {}nomax t : exists
s,
R t s /\ s <> t.
have /asboolP := nomax; rewrite asbool_neg => /forallp_asboolPn /(
_ t).
move=> /asboolP; rewrite asbool_neg => /existsp_asboolPn [s].
by move=> /asboolP; rewrite asbool_neg => /imply_asboolPn []; exists s.
have tot0 : total_on set0 R by [].
apply: (
ZL' (
exist _ set0 tot0))
R'tot_lub _ => // A.
have /Rtot_max [t tub] := svalP A; have [s [Rts snet]] := nomax t.
have Astot : total_on (
sval A `|` [set s])
R.
move=> u v [Au|->]; last first.
by move=> [/tub Rvt|->]; right=> //; apply: Rtrans Rts.
move=> [Av|->]; [apply: (
svalP A)
|left] => //.
by apply: Rtrans Rts; apply: tub.
exists (
exist _ (
sval A `|` [set s])
Astot)
; split; first by move=> ? ?; left.
split=> [AeAs|[B Btot] sAB sBAs].
have [/tub Rst|] := pselect (
sval A s)
; first exact/snet/Rantisym.
by rewrite AeAs /=; apply; right.
have [Bs|nBs] := pselect (
B s).
by right; apply: eq_exist; rewrite predeqE => r; split=> [/sBAs|[/sAB|->]].
left; case: A tub Astot sBAs sAB => A Atot /= tub Astot sBAs sAB.
apply: eq_exist; rewrite predeqE => r; split=> [Br|/sAB] //.
by have /sBAs [|ser] // := Br; rewrite ser in Br.
Qed.
Section
Zorn_subset
.
Variables (
T
: Type) (
P
: set (
set T)).
Lemma
Zorn_bigcup
:
(
forall
F
: set (
set T)
, F `<=` P -> total_on F subset ->
P (
\bigcup_(
X
in F)
X))
->
exists
A,
P A /\ forall
B,
A `<` B -> ~ P B.
Proof.
End Zorn_subset.
Definition
maximal_disjoint_subcollection
T
I
(
F
: I -> set T) (
A
B
: set I)
:=
[/\ A `<=` B, trivIset A F & forall
C,
A `<` C -> C `<=` B -> ~ trivIset C F ].
Section
maximal_disjoint_subcollection
.
Context {I
T
: Type}.
Variables (
B
: I -> set T) (
D
: set I).
Let
P
:= fun
X
=> X `<=` D /\ trivIset X B.
Let
maxP
(
A
: set (
set I))
:
A `<=` P -> total_on A (
fun
x
y
=> x `<=` y)
-> P (
\bigcup_(
x
in A)
x).
Proof.
move=> AP h; split; first by apply: bigcup_sub => E /AP [].
move=> i j [x Ax] xi [y Ay] yj ij; have [xy|yx] := h _ _ Ax Ay.
- by apply: (
AP _ Ay).
2 => //; exact: xy.
- by apply: (
AP _ Ax).
2 => //; exact: yx.
Qed.
Lemma
ex_maximal_disjoint_subcollection
:
{
E
| maximal_disjoint_subcollection B E D }.
Proof.
End maximal_disjoint_subcollection.
Definition
premaximal
T
(
R
: T -> T -> Prop) (
t
: T)
:=
forall
s,
R t s -> R s t.
Lemma
ZL_preorder
T
(
t0
: T) (
R
: T -> T -> Prop)
:
(
forall
t,
R t t)
-> (
forall
r
s
t,
R r s -> R s t -> R r t)
->
(
forall
A
: set T, total_on A R -> exists
t,
forall
s,
A s -> R s t)
->
exists
t,
premaximal R t.
Proof.
set Teq := @gen_eqMixin T; set Tch := @gen_choiceMixin T.
set Tp := Pointed.Pack (
Pointed.Class (
Choice.Class Teq Tch)
t0).
move=> Rrefl Rtrans tot_max.
set eqR := fun
s
t
=> R s t /\ R t s; set ceqR := fun
s
=> [set
t
| eqR s t].
have eqR_trans r s t : eqR r s -> eqR s t -> eqR r t.
by move=> [Rrs Rsr] [Rst Rts]; split; [apply: Rtrans Rst|apply: Rtrans Rsr].
have ceqR_uniq s t : eqR s t -> ceqR s = ceqR t.
by rewrite predeqE => - [Rst Rts] r; split=> [[Rr rR] | [Rr rR]]; split;
try exact: Rtrans Rr; exact: Rtrans rR _.
set ceqRs := ceqR @` setT; set quotR := sig ceqRs.
have ceqRP t : ceqRs (
ceqR t)
by exists t.
set lift := fun
t
=> exist _ (
ceqR t) (
ceqRP t).
have lift_surj (
A
: quotR)
: exists
t
: Tp, lift t = A.
case: A => A [t Tt ctA]; exists t; rewrite /lift; case : _ / ctA.
exact/congr1/Prop_irrelevance.
have lift_inj s t : eqR s t -> lift s = lift t.
by move=> eqRst; apply/eq_exist/ceqR_uniq.
have lift_eqR s t : lift s = lift t -> eqR s t.
move=> cst; have ceqst : ceqR s = ceqR t by have := congr1 sval cst.
by rewrite [_ s]ceqst; split; apply: Rrefl.
set repr := fun
A
: quotR => get [set
t
: Tp | lift t = A].
have repr_liftE t : eqR t (
repr (
lift t))
by apply: lift_eqR; have -> := getPex (
lift_surj (
lift t)).
set R' := fun
A
B
: quotR => R (
repr A) (
repr B).
have R'refl A : R' A A by apply: Rrefl.
have R'trans A B C : R' A B -> R' B C -> R' A C by apply: Rtrans.
have R'antisym A B : R' A B -> R' B A -> A = B.
move=> RAB RBA; have [t tA] := lift_surj A; have [s sB] := lift_surj B.
rewrite -tA -sB; apply: lift_inj; apply (
eqR_trans _ _ _ (
repr_liftE t)).
have eAB : eqR (
repr A) (
repr B)
by [].
rewrite tA; apply: eqR_trans eAB _; rewrite -sB.
by have [] := repr_liftE s.
have [A Atot|A Amax] := Zorn R'refl R'trans R'antisym.
have /tot_max [t tmax] : total_on [set repr B |
B
in A] R.
by move=> ?? [B AB <-] [C AC <-]; apply: Atot.
exists (
lift t)
=> B AB; have [Rt _] := repr_liftE t.
by apply: Rtrans Rt; apply: tmax; exists B.
exists (
repr A)
=> t RAt.
have /Amax <- : R' A (
lift t).
by have [Rt _] := repr_liftE t; apply: Rtrans Rt.
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].
Lemma
ubP
A
x
: (
forall
y,
A y -> (
y <= x)
%O)
<-> ubound A x.
Proof.
by []. Qed.
Lemma
lbP
A
x
: (
forall
y,
A y -> (
x <= y)
%O)
<-> lbound A x.
Proof.
by []. Qed.
Lemma
ub_set1
x
y
: ubound [set x] y = (
x <= y)
%O.
Proof.
Lemma
lb_set1
x
y
: lbound [set x] y = (
x >= y)
%O.
Proof.
Lemma
lb_ub_set1
x
y
: lbound (
ubound [set x])
y -> (
y <= x)
%O.
Proof.
by move/(
_ x)
; apply; rewrite ub_set1. Qed.
Lemma
ub_lb_set1
x
y
: ubound (
lbound [set x])
y -> (
x <= y)
%O.
Proof.
by move/(
_ x)
; apply; rewrite lb_set1. Qed.
Lemma
lb_ub_refl
x
: lbound (
ubound [set x])
x.
Proof.
by move=> y; apply. Qed.
Lemma
ub_lb_refl
x
: ubound (
lbound [set x])
x.
Proof.
by move=> y; apply. Qed.
Lemma
ub_lb_ub
A
x
y
: ubound A y -> lbound (
ubound A)
x -> (
x <= y)
%O.
Proof.
by move=> Ay; apply. Qed.
Lemma
lb_ub_lb
A
x
y
: lbound A y -> ubound (
lbound A)
x -> (
y <= x)
%O.
Proof.
by move=> Ey; apply. Qed.
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.
Lemma
has_ub_set1
x
: has_ubound [set x].
Proof.
Lemma
has_inf0
: ~ has_inf (
@set0 T).
Proof.
by rewrite /has_inf not_andP; left; apply/set0P/negP/negPn. Qed.
Lemma
has_sup0
: ~ has_sup (
@set0 T).
Proof.
by rewrite /has_sup not_andP; left; apply/set0P/negP/negPn. Qed.
Lemma
has_sup1
x
: has_sup [set x].
Proof.
by split; [exists x | exists x => y ->]. Qed.
Lemma
has_inf1
x
: has_inf [set x].
Proof.
by split; [exists x | exists x => y ->]. Qed.
Lemma
subset_has_lbound
A
B
: A `<=` B -> has_lbound B -> has_lbound A.
Proof.
by move=> AB [l Bl]; exists l => a Aa; apply/Bl/AB. Qed.
Lemma
subset_has_ubound
A
B
: A `<=` B -> has_ubound B -> has_ubound A.
Proof.
by move=> AB [l Bl]; exists l => a Aa; apply/Bl/AB. Qed.
Lemma
downP
A
x
: (
exists2
y,
A y & (
x <= y)
%O)
<-> down A x.
Proof.
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).
Lemma
supremums1
x
: supremums [set x] = [set x].
Proof.
Lemma
is_subset1_supremums
A
: is_subset1 (
supremums A).
Proof.
Definition
supremum
x0
A
:= if A == set0 then x0 else xget x0 (
supremums A).
Lemma
supremum_out
x0
A
: ~ has_sup A -> supremum x0 A = x0.
Proof.
move=> hsA; rewrite /supremum; case: ifPn => // /set0P[/= x Ax].
case: xgetP => //= _ -> [uA _]; exfalso.
by apply: hsA; split; [exists x|exists (
xget x0 (
supremums A))
].
Qed.
Lemma
supremum0
x0
: supremum x0 set0 = x0.
Proof.
by rewrite /supremum eqxx. Qed.
Lemma
supremum1
x0
x
: supremum x0 [set x] = x.
Proof.
Definition
infimums
A
:= lbound A `&` ubound (
lbound A).
Lemma
infimums1
x
: infimums [set x] = [set x].
Proof.
Lemma
is_subset1_infimums
A
: is_subset1 (
infimums A).
Proof.
Definition
infimum
x0
A
:= if A == set0 then x0 else xget x0 (
infimums A).
End UpperLowerTheory.
Section
UpperLowerOrderTheory
.
Import Order.TTheory.
Variables (
d
: unit) (
T
: orderType d).
Implicit Types (
A : set T) (
x y z : T).
Lemma
ge_supremum_Nmem
x0
A
t
:
supremums A !=set0 -> A t -> (
supremum x0 A >= t)
%O.
Proof.
case=> x Ax; rewrite /supremum; case: ifPn => [/eqP -> //|_].
by case: xgetP => [y yA [uAy _]|/(
_ x)
//]; exact: uAy.
Qed.
Lemma
le_infimum_Nmem
x0
A
t
:
infimums A !=set0 -> A t -> (
infimum x0 A <= t)
%O.
Proof.
case=> x Ex; rewrite /infimum; case: ifPn => [/eqP -> //|_].
by case: xgetP => [y yE [uEy _]|/(
_ x)
//]; exact: uEy.
Qed.
End UpperLowerOrderTheory.
Lemma
nat_supremums_neq0
(
A
: set nat)
: ubound A !=set0 -> supremums A !=set0.
Proof.
case => /=; elim => [A0|n ih]; first by exists O.
case: (
pselect (
ubound A n))
=> [/ih //|An {ih}] An1.
exists n.
+1; split => // m Am; case/existsNP : An => k /not_implyP[Ak /negP].
rewrite -Order.
TotalTheory.ltNge => kn.
by rewrite (
Order.POrderTheory.le_trans _ (
Am _ Ak)).
Qed.
Definition
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
.
Lemma
meetsC
T
(
F
G
: set (
set T))
: F `#` G = G `#` F.
Proof.
gen have sFG : F G / F `#` G -> G `#` F.
by move=> FG B A => /FG; rewrite setIC; apply.
by rewrite propeqE; split; apply: sFG.
Qed.
Lemma
sub_meets
T
(
F
F'
G
G'
: set (
set T))
:
F `<=` F' -> G `<=` G' -> F' `#` G' -> F `#` G.
Proof.
by move=> sF sG FG A B /sF FA /sG GB; apply: (FG A B). Qed.
Lemma
meetsSr
T
(
F
G
G'
: set (
set T))
:
G `<=` G' -> F `#` G' -> F `#` G.
Proof.
Lemma
meetsSl
T
(
G
F
F'
: set (
set T))
:
F `<=` F' -> F' `#` G -> F `#` G.
Proof.
by move=> /sub_meets; apply. Qed.
End meets.
Fact
set_display
: unit
Proof.
by []. Qed.
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).
Proof.
by apply/asboolP/eqP; rewrite setIidPl. Qed.
Lemma
lt_def
A
B
: `[< A `<` B >] = (
B != A)
&& `[< A `<=` B >].
Proof.
apply/idP/idP => [/asboolP|/andP[BA /asboolP AB]]; rewrite properEneq eq_sym;
by [move=> [] -> /asboolP|apply/asboolP].
Qed.
Lemma
joinKI
B
A
: A `&` (
A `|` B)
= A.
Proof.
Lemma
meetKU
B
A
: A `|` (
A `&` B)
= A.
Proof.
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.
Lemma
SetOrder_sub0set
A
: (
set0 <= A)
%O.
Proof.
by apply/asboolP; apply: sub0set. Qed.
Lemma
SetOrder_setTsub
A
: (
A <= setT)
%O.
Proof.
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].
Lemma
subKI
A
B
: B `&` (
A `\` B)
= set0.
Proof.
Lemma
joinIB
A
B
: (
A `&` B)
`|` A `\` B = A.
Proof.
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.
Lemma
subsetEset
A
B
: (
A <= B)
%O = (
A `<=` B)
:> Prop.
Proof.
Lemma
properEset
A
B
: (
A < B)
%O = (
A `<` B)
:> Prop.
Proof.
Lemma
subEset
A
B
: (
A `\` B)
%O = (
A `\` B)
Proof.
by []. Qed.
Lemma
complEset
A
: (
~` A)
%O = ~` A
Proof.
by []. Qed.
Lemma
botEset
: 0%O = @set0 T
Proof.
by []. Qed.
Lemma
topEset
: 1%O = @setT T
Proof.
by []. Qed.
Lemma
meetEset
A
B
: (
A `&` B)
%O = (
A `&` B)
Proof.
by []. Qed.
Lemma
joinEset
A
B
: (
A `|` B)
%O = (
A `|` B)
Proof.
by []. Qed.
Lemma
subsetPset
A
B
: reflect (
A `<=` B) (
A <= B)
%O.
Proof.
Lemma
properPset
A
B
: reflect (
A `<` B) (
A < B)
%O.
Proof.
End exports.
End Exports.
End SetOrder.
Export SetOrder.Exports.
Section
product
.
Variables (
T1
T2
: Type).
Implicit Type A B : set (
T1 * T2).
Lemma
subset_fst_set
: {homo @fst_set T1 T2 :
A
B
/ A `<=` B}.
Proof.
by move=> A B AB x [y Axy]; exists y; exact/AB. Qed.
Lemma
subset_snd_set
: {homo @snd_set T1 T2 :
A
B
/ A `<=` B}.
Proof.
by move=> A B AB x [y Axy]; exists y; exact/AB. Qed.
Lemma
fst_set_fst
A
: A `<=` A.
`1 \o fst
Proof.
by move=> [x y]; exists y. Qed.
Lemma
snd_set_snd
A:
A `<=` A.
`2 \o snd
Proof.
by move=> [x y]; exists x. Qed.
Lemma
fst_setM
(
X
: set T1) (
Y
: set T2)
: (
X `*` Y).
`1 `<=` X.
Proof.
by move=> x [y [//]]. Qed.
Lemma
snd_setM
(
X
: set T1) (
Y
: set T2)
: (
X `*` Y).
`2 `<=` Y.
Proof.
by move=> x [y [//]]. Qed.
Lemma
fst_setMR
(
X
: set T1) (
Y
: T1 -> set T2)
: (
X `*`` Y).
`1 `<=` X.
Proof.
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].
Lemma
xsection_snd_set
A
x
: xsection A x `<=` A.
`2.
Proof.
by move=> y Axy; exists x; rewrite /xsection/= inE in Axy. Qed.
Lemma
ysection_fst_set
A
y
: ysection A y `<=` A.
`1.
Proof.
by move=> x Axy; exists y; rewrite /ysection/= inE in Axy. Qed.
Lemma
mem_xsection
x
y
A
: (
y \in xsection A x)
= ((
x, y)
\in A).
Proof.
Lemma
mem_ysection
x
y
A
: (
x \in ysection A y)
= ((
x, y)
\in A).
Proof.
Lemma
xsection0
x
: xsection set0 x = set0.
Proof.
by rewrite predeqE /xsection => y; split => //=; rewrite inE. Qed.
Lemma
ysection0
y
: ysection set0 y = set0.
Proof.
by rewrite predeqE /ysection => x; split => //=; rewrite inE. Qed.
Lemma
in_xsectionM
X1
X2
x
: x \in X1 -> xsection (
X1 `*` X2)
x = X2.
Proof.
move=> xX1; apply/seteqP; split=> [y /xsection_snd_set|]; first exact: snd_setM.
by move=> y X2y; rewrite /xsection/= inE; split=> //=; rewrite inE in xX1.
Qed.
Lemma
in_ysectionM
X1
X2
y
: y \in X2 -> ysection (
X1 `*` X2)
y = X1.
Proof.
move=> yX2; apply/seteqP; split=> [x /ysection_fst_set|]; first exact: fst_setM.
by move=> x X1x; rewrite /ysection/= inE; split=> //=; rewrite inE in yX2.
Qed.
Lemma
notin_xsectionM
X1
X2
x
: x \notin X1 -> xsection (
X1 `*` X2)
x = set0.
Proof.
move=> xX1; rewrite /xsection /= predeqE => y; split => //.
by rewrite /xsection/= inE => -[] /=; rewrite notin_set in xX1.
Qed.
Lemma
notin_ysectionM
X1
X2
y
: y \notin X2 -> ysection (
X1 `*` X2)
y = set0.
Proof.
move=> yX2; rewrite /xsection /= predeqE => x; split => //.
by rewrite /ysection/= inE => -[_]; rewrite notin_set in yX2.
Qed.
Lemma
xsection_bigcup
(
F
: nat -> set (
T1 * T2))
x
:
xsection (
\bigcup_n F n)
x = \bigcup_n xsection (
F n)
x.
Proof.
rewrite predeqE /xsection => y; split => [|[n _]] /=; rewrite inE.
by move=> -[n _ Fnxy]; exists n => //=; rewrite inE.
by move=> Fnxy; rewrite inE; exists n.
Qed.
Lemma
ysection_bigcup
(
F
: nat -> set (
T1 * T2))
y
:
ysection (
\bigcup_n F n)
y = \bigcup_n ysection (
F n)
y.
Proof.
rewrite predeqE /ysection => x; split => [|[n _]] /=; rewrite inE.
by move=> -[n _ Fnxy]; exists n => //=; rewrite inE.
by move=> Fnxy; rewrite inE; exists n.
Qed.
Lemma
trivIset_xsection
(
F
: nat -> set (
T1 * T2))
x
: trivIset setT F ->
trivIset setT (
fun
n
=> xsection (
F n)
x).
Proof.
move=> /trivIsetP h; apply/trivIsetP => i j _ _ ij.
rewrite /xsection /= predeqE => y; split => //= -[]; rewrite !inE => Fixy Fjxy.
by have := h i j Logic.I Logic.I ij; rewrite predeqE => /(
_ (
x, y))
[+ _]; apply.
Qed.
Lemma
trivIset_ysection
(
F
: nat -> set (
T1 * T2))
y
: trivIset setT F ->
trivIset setT (
fun
n
=> ysection (
F n)
y).
Proof.
move=> /trivIsetP h; apply/trivIsetP => i j _ _ ij.
rewrite /ysection /= predeqE => x; split => //= -[]; rewrite !inE => Fixy Fjxy.
by have := h i j Logic.I Logic.I ij; rewrite predeqE => /(
_ (
x, y))
[+ _]; apply.
Qed.
Lemma
le_xsection
x
: {homo xsection ^~ x :
X
Y
/ X `<=` Y >-> X `<=` Y}.
Proof.
by move=> X Y XY y; rewrite /xsection /= 2!inE => /XY. Qed.
Lemma
le_ysection
y
: {homo ysection ^~ y :
X
Y
/ X `<=` Y >-> X `<=` Y}.
Proof.
by move=> X Y XY x; rewrite /ysection /= 2!inE => /XY. Qed.
Lemma
xsectionI
A
B
x
: xsection (
A `&` B)
x = xsection A x `&` xsection B x.
Proof.
by rewrite /xsection predeqE => y/=; split; rewrite !inE => -[]. Qed.
Lemma
ysectionI
A
B
y
: ysection (
A `&` B)
y = ysection A y `&` ysection B y.
Proof.
by rewrite /ysection predeqE => x/=; split; rewrite !inE => -[]. Qed.
Lemma
xsectionD
X
Y
x
: xsection (
X `\` Y)
x = xsection X x `\` xsection Y x.
Proof.
by rewrite predeqE /xsection /= => y; split; rewrite !inE. Qed.
Lemma
ysectionD
X
Y
y
: ysection (
X `\` Y)
y = ysection X y `\` ysection Y y.
Proof.
by rewrite predeqE /ysection /= => x; split; rewrite !inE. Qed.
Lemma
xsection_preimage_snd
(
B
: set T2)
x
: xsection (
snd @^-1` B)
x = B.
Proof.
by apply/seteqP; split; move=> y/=; rewrite /xsection/= inE. Qed.
Lemma
ysection_preimage_fst
(
A
: set T1)
y
: ysection (
fst @^-1` A)
y = A.
Proof.
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.
Lemma
set_compose_subset
{X
Y
: Type} (
A
C
: set (
X * Y)) (
B
D
: set (
Y * X))
:
A `<=` C -> B `<=` D -> A \; B `<=` C \; D.
Proof.
by move=> AsubC BD [x z] /= [y] Bxy Ayz; exists y; [exact: BD | exact: AsubC].
Qed.
Lemma
set_compose_diag
{X : Type} (
E
: set (
X * X))
:
E \; range (
fun
x
=> (
x, x))
= E.
Proof.
rewrite eqEsubset; split => [[_ _] [_ [_ _ [<- <-//]]]|[x y] Exy]/=.
by exists x => //; exists x.
Qed.