A. Lemma-setc_ni-x, ~inc x (A -s B) -> (~ inc x A \/ inc x B)

A. Lemma-set_cu2, X -s (A\cup B) = (X -s A) \cap (X -s B)

A. Lemma-set_ci2, X -s (A\cap B) = (X -s A) \cup (X -s B)

A. Lemma-set_cc, s (A -s B)) = (E -s A) \cup B. Lemma setI2_Cr A B : (A \cap B) \cup (A -s B) = A

A. Lemma-setcu2_l, A \cup B) -s C = (A -s C) \cup (B -s C)

A. Lemma-setcu2_r, A -s (B \cup C) = (A -s B) \cap (A -s C)

A. Lemma-setci2_l, A \cap B) -s C = (A -s C) \cap (B -s C)

&. D2 and P. }. , := (prop_when11 d1 d2 (inPhantom P)) (at level 0, format "{ 'when' d1 & d2

. Lemma-fun_on_quotient_pr-r-f-x, Vf f x = fun_on_rep (fun _ => Vf f x) (Vf (canon_proj r)x)

. Lemma-induced_rel_classp-x, (classp (induced_relation r a) x <-> exists y, [/\ classp r y, nonempty (y \cap a) & x =

J. Grimm, inc a (A \cap A') by fprops. have bAA: inc b (A \cap A'') by fprops. case (equal_or_not A' A'') => aux. case (i2 _ _ AX AX')=> // ss. rewrite -aux in bAA; elim nab

_. Ax, case; first by move=> h; empty_tac1 a; aw. case; first by move=> h; empty_tac1 b; aw. case; first by move=> h; empty_tac1 t; aw. move=> [h1 h2]. rewrite -h1 in bAA. case (i2 _ _ AX AX')=>// ss. elim nab; by apply: (ss _ _ aAA bAA). move=> tA; apply: Zo_i. rewrite -uXE;apply: (@setU_i _ A)=>

. Part-c, We do not know how to generalize. The last claim is obvious Assume R intransitive of order p ? 3, let q > p and consider q distinct elements, which are related (with the exception of x q?1 and x q ; discard the q ? p first elements. The missing relation is true by intransitivity

B. ?x?y, ?z(z ? y) and y ? x and ?u[bu ? x =? ?v[v ? x and ?t (t ? v ?? t

A. ?a{, ?x(x ? a =? x = ) and ?x?y(x ? a and y ? a =? x = y or x ? y = )] =? ?b?x?u

A. ?x, = =? ?y(y ? x and y ? x = )] (Axiom of foundation)

B. Comments, . B2, B. B3, S. B0, B. B2 et al., From SS, one can deduce SC and B0. The Zermelo theory consists in B1, It is a weaker theory. Axiom AF is independent of all other axioms, it excludes some José Grimm Definition intersectiont, ->Set):= by_cases(fun H:nonemptyT In => Zo (f (chooseT_any H)) (fun y => forall z : In, inc y

J. Parameter and . Set, Axiom axiom_of_pair : forall x y x' y' : Set, (J x y = J x' y') -> (x = x' & y = y')

. Correspondences, In a first implementation, a correspondence was a set, more precisely, a functional graph on a set with three elements, Source, Target and Graph. Definition create x y g:= denote Source x (denote Target y (denote Graph g stop))

F. Bourbaki, and whose graph F is such that the relation (x, y) ? F is an equivalence relation on E. Note: the correspondence is uniquely defined by F, since E is the substrate of F; conversely, given an equivalence F on E, the domain and range of F is E, thus F ? E×E, and (E, E, F) is a correspondence

G. @bullet-?1-g-?-», Proposition 3 (compg_inverse) « Let G, G ? be two graphs. The inverse of G ? ?G is then ?1

G. ?g?a??, Proposition 5 (compg_image) says

Y. Bertod and P. Castéran, Interactive Theorem Proving and Program Development, 2004.
DOI : 10.1007/978-3-662-07964-5

N. Bourbaki, Theory of Sets, Elements of Mathematics, 1968.

N. Bourbaki, Éléments de mathématiques, Théorie des ensembles, Diffusion CCLS, 1970.

J. Krivine, Théorie axiomatique des ensembles, 1972.

E. Nelson, Internal set theory: A new approach to nonstandard analysis, Bulletin of the American Mathematical Society, vol.83, issue.6, 1977.
DOI : 10.1090/S0002-9904-1977-14398-X