Definition card_six := csucc card_five. Notation "\5c" := card_five. Notation "\6c ,
Variable u: Set. Hypothesis Sr: isr S = prod_of_relation r1 r2. Hypothesis Sr': isr S' = prod_of_relation r1 r2 ,
Whenever ? ? L, equations (3.23) hold ,
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) ,
n := domain x): inc x ex4_F -> [/\ n <> \0c, ex4_seqp x n & forall i, i<c n -> pairp ,
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) ,
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 ,
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) ,
= 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) ,
gle (psr S) i j -> inc y (Vg Gf i) -> (* 4 *) exists2 x, inc x (Vg Gf j) & y = Vf ,
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) ,
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 ,
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 ,
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 ,
Vg Er k) (ex5_Y J k x)) (ex5m J k x). (* 25 *) Lemma ex5_res1b J k x, pp.5-6 ,
Vg Gf k) (fun y => gle (Vg Er k) y (ex5m J k x)). (* 22 *) ,
Definition ex5_coherent2 x := [/\ ex5_coh2 (domain x) x, sub (domain x) (psI S) ,
:= domain x Hypothesis coh2: ex5_coherent2 x. Hypothesis jJ : inc j (psI S) /\ ~ (inc j J') ,
Definition ex6_Fl i := inductive_limit (ex6_systemi i) ,
H: inc i L): ex6_Fl i = inductive_limit (inl_restr (ex6_prop4 H) ,
H:inc i L): inl_same_data (ex6_systemi i) (inl_restr (ex6_prop4 H)) ,
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)) ,
H:inc i L): inl_equiv (ex6_systemi i) = inl_equiv (inl_restr (ex6_prop4 H)) ,
H:gle rL i j): inl_equiv (ex6_systemi i) = inl_equiv (inl_restr (ex6_prop5c H)) ,
H: gle rL i j): ex6_Fl i = (inductive_limit (inl_restr (ex6_prop5b H))) ,
H:gle rL i j): ex6_gij (J i j) = inl_restr_cf (ex6_prop5c H) ,
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) ,
Variable (u:Set) ,
:= inl_system_product same_I): inl_subfam_hyp S'' (Lg (isI S) (fun i => graph (Vg u i))) ,
É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. ,
Éléments de mathématiques, I les structures fondamentales de l'analyse, Livre 1 Théorie des ensembles, 1957. ,
Theory of Sets, Elements of Mathematics, 1968. ,
Éléments de mathématiques, Théorie des ensembles, Diffusion CCLS, 1970. ,
Elements of Mathematics, Algebra I, 1989. ,
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
Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets, 2009. ,
Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers, 2009. ,