Module mathcomp.classical.classical_sets

# 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 | `` `+` `` |==| symmetric difference | `` ~` `` |==| set complement | `` `<=` `` |==| $\subseteq$ | `` f @` A `` |==| image by f of A | `` f @^-1` A `` |==| preimage by f of A | [set x] |==| the singleton set $\{x\}$ | [set~ x] |==| the complement of $\{x\}$ | [set E \| x in P] |==| the set of E with x ranging in P | range f |==| image by f of the full set | \big[setU/set0]_(i <- s \| P i) f i |==| finite union | \bigcup_(k in P) F k |==| 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 >= n) F := \bigcup_(i in [set i | i >= n]) F \bigcup_i F == same as before with T left implicit \bigcap_(i in P) F == intersection of the elements of the family F whose index satisfies P \bigcap_(i : T) F == union of the family F indexed on T \bigcap_(i < n) F := \bigcap_(i in `I_n) F \bigcap_(i >= n) F := \bigcap_(i in [set i | i >= n]) F \bigcap_i F == same as before with T left implicit 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 The HB class is Pointed. point == canonical inhabitant of a pointedType get P == point x in P if it exists, point otherwise P must be a set on a pointedType. ``` ## squash/unsquash ``` $| T | == the type `T : Type` is inhabited $| T | has type `Prop`. $| T | is a notation for `squashed T`. squash x == object of type $| T | (with x : T) unsquash s == extract an inhabitant of type `T` (with s : $| T |) ``` Tactic: - squash x: solves a goal $| T | by instantiating with x or [the T of x] ## Pairwise-disjoint sets ``` trivIset D F == the sets F i, where i ranges over D : set I, are pairwise-disjoint cover D F := \bigcup_(i in D) F i partition D F A == the non-empty sets F i,where i ranges over D : set I, form a partition of A pblock_index D F x == index i such that i \in D and x \in F i pblock D F x := F (pblock_index D F x) maximal_disjoint_subcollection F A B == A is a maximal (for inclusion) disjoint subcollection of the collection B of elements in F : I -> set T ``` ## Upper and lower bounds ``` ubound A == the set of upper bounds of the set A lbound A == the set of lower bounds of the set A ``` Predicates to express existence conditions of supremum and infimum of sets of real numbers: ``` has_ubound A := ubound A != set0 has_sup A := A != set0 /\ has_ubound A has_lbound A := lbound A != set0 has_inf A := A != set0 /\ has_lbound A isLub A m := m is a least upper bound of the set A supremums A := set of supremums of the set A supremum x0 A == supremum of A or x0 if A is empty infimums A := set of infimums of the set A infimum x0 A == infimum of A or x0 if A is empty F `#` G := the classes of sets F and G intersect ``` ## Sections ``` xsection A x == with A : set (T1 * T2) and x : T1 is the x-section of A ysection A y == with A : set (T1 * T2) and y : T2 is the y-section of A ``` ## Relations Notations for composition and inverse (scope: relation_scope): ``` B \; A == [set x | exists z, A (x.1, z) & B (z, x.2)] A^-1 == [set xy | A (xy.2, xy.1)] ```