=. Card_six, Definition card_six := csucc card_five. Notation "\5c" := card_five. Notation "\6c

S. Variables and . Inductive_system, Variable u: Set. Hypothesis Sr: isr S = prod_of_relation r1 r2. Hypothesis Sr': isr S' = prod_of_relation r1 r2

S. Introduce, Whenever ? ? L, equations (3.23) hold

. Lemma-inl_dl2_res1-lam, inc lam I2 -> inl_same_index (inl_dl2_Slambda lam) (inl_dl2_Slambda' lam) /\ inl_map2_compat (inl_dl2_Slambda lam) (inl_dl2_Slambda' lam)

. Lemma-ex4_inf_hi-x, n := domain x): inc x ex4_F -> [/\ n <> \0c, ex4_seqp x n & forall i, i<c n -> pairp

F. We and . ??, This function is obtained by truncating its argument to the j first terms (operation that obvious yields an element of F) then modifying the value of r . This yields an element of F provided that the new value is ? r (x) (in order to preserve r < s)

. Lemma-ex4_f_stable_modify_r-x-i, inc x ex4_F -> gle r i (ex4_fct_r x) -> (forall k, k <c cpred (ex4_length x) -> ~ gle r i (Vg x (cdouble k))) -> inc

. Lemma-ex4_compose_f-i-j-k, psf := ex4_function_f_fam): gle r i j -> gle r j k -> Vg psf (J i j) \co Vg psf (J j k) = Vg psf (J i k)

?. Assume, = f ab (z) and y = f bc (z) This means that x and y are obtained by restricting z to size j and j and modifying r . If x and y have the same length, then j = j . As s is not modified, we have s(x) = s(y) This shows (b)

. Lemma-ex5_gij_prop2-i-j-y, gle (psr S) i j -> inc y (Vg Gf i) -> (* 4 *) exists2 x, inc x (Vg Gf j) & y = Vf

. Lemma-ex5_xij_pr-i-j-x, gle (psr S) i j -> forall t, inc t (ex5_X i j x) <-> (inc t (Vg (psE S) j) /\ x = Vf (ex5_f i j) t)

. Lemma-ex5_mij_pr1-i-j-x, M:= ex5_M i j x): gle (psr S) i j -> inc x (Vg Gf i) -> inc M (ex5_X i j x) /\ forall t, inc t (ex5_X i j x) -> gle

. Lemma-ex5_mij_pr2-i-j-x, M:= ex5_M i j x): (* 3 *) gle (psr S) i j -> inc x (Vg Gf i) -> Vf (ex5_f i j) M = x /\ forall t, inc t (Vg (psE S) j) -> Vf

. Obviously, If i ? J then m ? k M i k (x k ), so that f i k (t ) ? i f i k (M i k (x k )) = x i . Now, f i k (t ) ? G i since t ? G k . Apply property G 5 to f i k (t ) ? i x i ; we get f i k (t ) = x i

J. Lemma-ex5_res1a, Vg Er k) (ex5_Y J k x)) (ex5m J k x). (* 25 *) Lemma ex5_res1b J k x, pp.5-6

. Zo, Vg Gf k) (fun y => gle (Vg Er k) y (ex5m J k x)). (* 22 *)

K. J. Definition-finite_ne_sub, K. , K. , and K. , Definition ex5_coherent2 x := [/\ ex5_coh2 (domain x) x, sub (domain x) (psI S)

J. Let, := domain x Hypothesis coh2: ex5_coherent2 x. Hypothesis jJ : inc j (psI S) /\ ~ (inc j J')

|. and _. =>-s-end, Definition ex6_Fl i := inductive_limit (ex6_systemi i)

. Lemma-ex6_res0-i, H: inc i L): ex6_Fl i = inductive_limit (inl_restr (ex6_prop4 H)

. Lemma-ex6_prop5a-i, H:inc i L): inl_same_data (ex6_systemi i) (inl_restr (ex6_prop4 H))

. Lemma-ex6_prop5c-i-j, gle rL i j -> sub_right_directed (Vg Jf i) (isr (ex6_systemi j)). (* 10 *) Lemma ex6_prop5d i j (H:gle rL i j): inl_same_data (ex6_systemi i) (inl_restr (ex6_prop5c H))

. Lemma-ex6_prop6a-i, H:inc i L): inl_equiv (ex6_systemi i) = inl_equiv (inl_restr (ex6_prop4 H))

. Lemma-ex6_prop6b-i-j, H:gle rL i j): inl_equiv (ex6_systemi i) = inl_equiv (inl_restr (ex6_prop5c H))

. Lemma-ex6_res1-i-j, H: gle rL i j): ex6_Fl i = (inductive_limit (inl_restr (ex6_prop5b H)))

. Lemma-ex6_gij_prop1-i-j, H:gle rL i j): ex6_gij (J i j) = inl_restr_cf (ex6_prop5c H)

?. ?. Lim, ?. ?. If-x-?-lim, and ?. J. , y, i ), j ) Write this as x = W(y, i , j, Note that the value of Inria Definition ex7_iso := Lf ex7_fct (inductive_limit ex7_system) (inductive_limit S)

S. Variables and . Inductive_system, Variable (u:Set)

. Lemma-ex8_inl_subfm_hyp-(-s-'', := inl_system_product same_I): inl_subfam_hyp S'' (Lg (isI S) (fun i => graph (Vg u i)))

N. Bourbaki, Éléments de mathématiques, I les structures fondamentales de l'analyse, Livre 1 Théorie des ensembles, Chapitre 3 Ensembles ordonnés, cardinaux, nombres entiers, 1956.

N. Bourbaki, Éléments de mathématiques, I les structures fondamentales de l'analyse, Livre 1 Théorie des ensembles, 1957.

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

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

N. Bourbaki, Elements of Mathematics, Algebra I, 1989.

F. Garillot, G. Gonthier, A. Mahboubi, and L. Rideau, Packaging Mathematical Structures, Theorem Proving in Higher Order Logics, 2009.
DOI : 10.1007/978-3-540-68103-8_11
URL : https://hal.archives-ouvertes.fr/inria-00368403

J. Grimm, Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets, 2009.

J. Grimm, Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers, 2009.