~inc x (A -s B) -> (~ inc x A \/ inc x B) ,
X -s (A\cup B) = (X -s A) \cap (X -s B) ,
X -s (A\cap B) = (X -s A) \cup (X -s B) ,
s (A -s B)) = (E -s A) \cup B. Lemma setI2_Cr A B : (A \cap B) \cup (A -s B) = A ,
A \cup B) -s C = (A -s C) \cup (B -s C) ,
A -s (B \cup C) = (A -s B) \cap (A -s C) ,
A \cap B) -s C = (A -s C) \cap (B -s C) ,
:= (prop_when11 d1 d2 (inPhantom P)) (at level 0, format "{ 'when' d1 & d2 ,
Vf f x = fun_on_rep (fun _ => Vf f x) (Vf (canon_proj r)x) ,
(classp (induced_relation r a) x <-> exists y, [/\ classp r y, nonempty (y \cap a) & x = ,
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 ,
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)=> ,
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 ,
?z(z ? y) and y ? x and ?u[bu ? x =? ?v[v ? x and ?t (t ? v ?? t ,
?x(x ? a =? x = ) and ?x?y(x ? a and y ? a =? x = y or x ? y = )] =? ?b?x?u ,
= =? ?y(y ? x and y ? x = )] (Axiom of foundation) ,
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 ,
Axiom axiom_of_pair : forall x y x' y' : Set, (J x y = J x' y') -> (x = x' & y = y') ,
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)) ,
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 ,
Proposition 3 (compg_inverse) « Let G, G ? be two graphs. The inverse of G ? ?G is then ?1 ,
Proposition 5 (compg_image) says ,
Interactive Theorem Proving and Program Development, 2004. ,
DOI : 10.1007/978-3-662-07964-5
Theory of Sets, Elements of Mathematics, 1968. ,
Éléments de mathématiques, Théorie des ensembles, Diffusion CCLS, 1970. ,
Théorie axiomatique des ensembles, 1972. ,
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