New files Subset_system_def.v, Subset_any.v, Function.v, Topology.v.

(Some are still embryonic)

Lebesgue/Function.v

+(**
+This file is part of the Elfic library
+
+Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
+
+This library is free software; you can redistribute it and/or
+modify it under the terms of the GNU Lesser General Public
+License as published by the Free Software Foundation; either
+version 3 of the License, or (at your option) any later version.
+
+This library is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+COPYING file for more details.
+*)
+
+(** Operations on functions (definitions and properties).
+
+  Subsets of the type U are represented by their belonging function,
+  of type U -> Prop.
+
+  Most of the properties are tautologies, and can be found on Wikipedia:
+  https://en.wikipedia.org/wiki/List_of_set_identities_and_relations *)
+
+From Coq Require Import FunctionalExtensionality.
+
+Require Import Subset Subset_finite Subset_seq Subset_any.
+
+
+Section Base_Def.
+
+Context {U1 U2 : Type}. (* Universes. *)
+
+Variable f g : U1 -> U2. (* Functions. *)
+
+Definition same_fun : Prop := forall x, f x = g x.
+
+Variable A1 : U1 -> Prop. (* Subset. *)
+Variable A2 : U2 -> Prop. (* Subset. *)
+
+Inductive image : U2 -> Prop := Im : forall x1, A1 x1 -> image (f x1).
+
+Definition image_ex : U2 -> Prop :=
+  fun x2 => exists x1, A1 x1 /\ x2 = f x1.
+
+Definition preimage : U1 -> Prop := fun x1 => A2 (f x1).
+
+Context {U3 : Type}. (* Universe. *)
+
+Variable f23 : U2 -> U3. (* Function. *)
+Variable f12 : U1 -> U2. (* Function. *)
+
+Definition compose : U1 -> U3 := fun x1 => f23 (f12 x1).
+
+End Base_Def.
+
+
+Section Prop_Facts0.
+
+Context {U1 U2 : Type}. (* Universes. *)
+
+(** Extensionality of functions. *)
+
+Lemma fun_ext : forall (f g : U1 -> U2), same_fun f g -> f = g.
+Proof.
+exact functional_extensionality.
+Qed.
+
+(** Facts about same_fun. *)
+
+(** It is an equivalence binary relation. *)
+
+(* Useless?
+Lemma same_fun_refl :
+  forall (f : U1 -> U2),
+    same_fun f f.
+Proof.
+easy.
+Qed.*)
+
+(* Useful? *)
+Lemma same_fun_sym :
+  forall (f g : U1 -> U2),
+    same_fun f g -> same_fun g f.
+Proof.
+easy.
+Qed.
+
+Lemma same_fun_trans :
+  forall (f g h : U1 -> U2),
+    same_fun f g -> same_fun g h -> same_fun f h.
+Proof.
+intros f g h H1 H2 x; now rewrite (H1 x).
+Qed.
+
+End Prop_Facts0.
+
+
+Ltac fun_unfold :=
+  repeat unfold
+    same_fun, (* Predicate. *)
+    compose, preimage. (* Constructors. *)
+
+Ltac fun_auto :=
+  fun_unfold; subset_auto.
+
+Ltac fun_ext_auto x :=
+  apply fun_ext; intros x; fun_auto.
+
+
+Section Image_Facts.
+
+(** Facts about images. *)
+
+Context {U1 U2 : Type}. (* Universes. *)
+
+Variable f g : U1 -> U2. (* Functions. *)
+
+Lemma image_eq : forall A1, image f A1 = image_ex f A1.
+Proof.
+intros; subset_ext_auto x2 Hx2; induction Hx2 as [x1 Hx1].
+exists x1; easy.
+rewrite (proj2 Hx1); easy.
+Qed.
+
+Lemma image_ext_fun : forall A1, same_fun f g -> image f A1 = image g A1.
+Proof.
+intros; subset_ext_auto x2 Hx2; induction Hx2 as [x1 Hx1];
+    [rewrite H | rewrite <- H]; easy.
+Qed.
+
+Lemma image_ext : forall A1 B1, same A1 B1 -> image f A1 = image f B1.
+Proof.
+intros A1 B1 H.
+subset_ext_auto x2 Hx2; induction Hx2 as [x1 Hx1]; apply Im; apply H; easy.
+Qed.
+
+Lemma image_empty_equiv :
+  forall A1, empty (image f A1) <-> empty A1.
+Proof.
+intros A1; split; intros HA1.
+intros x1 Hx1; apply (HA1 (f x1)); easy.
+intros x2 [x1 Hx1]; apply (HA1 x1); easy.
+Qed.
+
+Lemma image_emptyset : image f emptyset = emptyset.
+Proof.
+apply empty_emptyset, image_empty_equiv; easy.
+Qed.
+
+Lemma image_monot :
+  forall A1 B1, incl A1 B1 -> incl (image f A1) (image f B1).
+Proof.
+intros A1 B1 H1 x2 [x1 Hx1]; apply Im, H1; easy.
+Qed.
+
+Lemma image_union :
+  forall A1 B1, image f (union A1 B1) = union (image f A1) (image f B1).
+Proof.
+intros A1 B1; apply subset_ext_equiv; split; intros x2.
+intros [x1 [Hx1 | Hx1]]; [left | right]; easy.
+intros [[x1 Hx1] | [x1 Hx1]]; apply Im; [left | right]; easy.
+Qed.
+
+Lemma image_inter :
+  forall A1 B1, incl (image f (inter A1 B1)) (inter (image f A1) (image f B1)).
+Proof.
+intros A1 B1 x2 [x1 Hx1]; split; apply Im, Hx1.
+Qed.
+
+Lemma image_diff :
+  forall A1 B1, incl (diff (image f A1) (image f B1)) (image f (diff A1 B1)).
+Proof.
+intros A1 B1 x2 [[x1 Hx1] Hx2']; apply Im; split; try easy.
+intros Hx1'; apply Hx2'; easy.
+Qed.
+
+Lemma image_compl : forall A1, incl (diff (image f fullset) (image f A1)) (image f (compl A1)).
+Proof.
+intros; rewrite compl_equiv_def_diff; apply image_diff.
+Qed.
+
+Lemma image_sym_diff :
+  forall A1 B1,
+    incl (sym_diff (image f A1) (image f B1)) (image f (sym_diff A1 B1)).
+Proof.
+intros; unfold sym_diff; rewrite image_union.
+apply union_monot; apply image_diff.
+Qed.
+
+Lemma image_union_finite_distr :
+  forall A1 N,
+    image f (union_finite A1 N) = union_finite (fun n => image f (A1 n)) N.
+Proof.
+intros A1 N; apply subset_ext_equiv; split; intros x2.
+intros [x1 [n [Hn Hx1]]]; exists n; split; easy.
+intros [n [Hn [x1 Hx1]]]; apply Im; exists n; easy.
+Qed.
+
+Lemma image_inter_finite :
+  forall A1 N,
+    incl (image f (inter_finite A1 N))
+      (inter_finite (fun n => image f (A1 n)) N).
+Proof.
+intros A1 N x2 [x1 Hx1] n Hn; apply Im, Hx1; easy.
+Qed.
+
+Lemma image_union_seq_distr :
+  forall A1, image f (union_seq A1) = union_seq (fun n => image f (A1 n)).
+Proof.
+intros A1; apply subset_ext_equiv; split; intros x2.
+intros [x1 [n Hx1]]; exists n; easy.
+intros [n [x1 Hx1]]; apply Im; exists n; easy.
+Qed.
+
+Lemma image_inter_seq :
+  forall A1,
+    incl (image f (inter_seq A1)) (inter_seq (fun n => image f (A1 n))).
+Proof.
+intros A1 x2 [x1 Hx1] n; apply Im, Hx1.
+Qed.
+
+End Image_Facts.
+
+
+Section Preimage_Facts.
+
+(** Facts about preimages. *)
+
+Context {U1 U2 : Type}. (* Universes. *)
+
+Variable f g : U1 -> U2. (* Functions. *)
+
+Lemma preimage_ext_fun :
+  forall A2, same_fun f g -> preimage f A2 = preimage g A2.
+Proof.
+intros A2 H; fun_ext_auto x1; rewrite (H x1); easy.
+Qed.
+
+Lemma preimage_ext :
+  forall A2 B2, same A2 B2 -> preimage f A2 = preimage f B2.
+Proof.
+intros; subset_ext_auto; fun_auto.
+Qed.
+
+Lemma preimage_empty_equiv :
+  forall A2, empty (preimage f A2) <-> disj A2 (image f fullset).
+Proof.
+intros A2; split.
+intros HA2 x2 Hx2a Hx2b; induction Hx2b as [x1 Hx1]; apply (HA2 x1); easy.
+intros HA2 x1 Hx1; apply (HA2 (f x1)); easy.
+Qed.
+
+Lemma preimage_emptyset : preimage f emptyset = emptyset.
+Proof.
+apply empty_emptyset, preimage_empty_equiv; easy.
+Qed.
+
+Lemma preimage_full_equiv :
+  forall A2, full (preimage f A2) <-> incl (image f fullset) A2.
+Proof.
+intros A2; split; intros HA2.
+intros x2 [x1 Hx1]; apply HA2.
+intros x1; apply HA2; easy.
+Qed.
+
+Lemma preimage_monot :
+  forall A2 B2, incl A2 B2 -> incl (preimage f A2) (preimage f B2).
+Proof.
+intros; fun_auto.
+Qed.
+
+Lemma preimage_compl :
+  forall A2, preimage f (compl A2) = compl (preimage f A2).
+Proof.
+intros; subset_ext_auto.
+Qed.
+
+Lemma preimage_union :
+  forall A2 B2,
+    preimage f (union A2 B2) = union (preimage f A2) (preimage f B2).
+Proof.
+intros; subset_ext_auto.
+Qed.
+
+Lemma preimage_inter :
+  forall A2 B2,
+    preimage f (inter A2 B2) = inter (preimage f A2) (preimage f B2).
+Proof.
+intros; subset_ext_auto.
+Qed.
+
+Lemma preimage_diff :
+  forall A2 B2,
+    preimage f (diff A2 B2) = diff (preimage f A2) (preimage f B2).
+Proof.
+intros; subset_ext_auto.
+Qed.
+
+Lemma preimage_sym_diff :
+  forall A2 B2,
+    preimage f (sym_diff A2 B2) = sym_diff (preimage f A2) (preimage f B2).
+Proof.
+intros; subset_ext_auto.
+Qed.
+
+Lemma preimage_cst :
+  forall A2 (x2 : U2), preimage (fun _ : U1 => x2) A2 = Prop_cst (A2 x2).
+Proof.
+intros; subset_ext_auto.
+Qed.
+
+Lemma preimage_union_finite_distr :
+  forall A2 N,
+    preimage f (union_finite A2 N) = union_finite (fun n => preimage f (A2 n)) N.
+Proof.
+intros; subset_ext_auto.
+Qed.
+
+Lemma preimage_inter_finite_distr :
+  forall A2 N,
+    preimage f (inter_finite A2 N) = inter_finite (fun n => preimage f (A2 n)) N.
+Proof.
+intros; subset_ext_auto.
+Qed.
+
+Lemma preimage_union_seq_distr :
+  forall A2,
+    preimage f (union_seq A2) = union_seq (fun n => preimage f (A2 n)).
+Proof.
+intros; subset_ext_auto.
+Qed.
+
+Lemma preimage_inter_seq_distr :
+  forall A2,
+    preimage f (inter_seq A2) = inter_seq (fun n => preimage f (A2 n)).
+Proof.
+intros; subset_ext_auto.
+Qed.
+
+End Preimage_Facts.
+
+
+Section Image_Preimage_Facts.
+
+(** Facts about images and preimages. *)
+
+Context {U1 U2 : Type}. (* Universes. *)
+
+Variable f : U1 -> U2. (* Function. *)
+
+Lemma image_of_preimage :
+  forall A2, image f (preimage f A2) = inter A2 (image f fullset).
+Proof.
+intros A2; apply subset_ext; intros x2; split.
+intros Hx2; induction Hx2 as [x1 Hx1]; easy.
+intros [Hx2 Hx2']; induction Hx2' as [x1 Hx1]; easy.
+Qed.
+
+Lemma image_of_preimage_of_image :
+  forall A1, image f (preimage f (image f A1)) = image f A1.
+Proof.
+intros; rewrite image_of_preimage; apply inter_left, image_monot; easy.
+Qed.
+
+Lemma preimage_of_image : forall A1, incl A1 (preimage f (image f A1)).
+Proof.
+easy.
+Qed.
+
+Lemma preimage_of_image_full : preimage f (image f fullset) = fullset.
+Proof.
+apply subset_ext_equiv; easy.
+Qed.
+
+Lemma preimage_of_image_of_preimage :
+  forall A2, preimage f (image f (preimage f A2)) = preimage f A2.
+Proof.
+intros; rewrite image_of_preimage.
+rewrite preimage_inter, preimage_of_image_full.
+apply inter_full_r.
+Qed.
+
+Lemma preimage_of_image_equiv :
+  forall A1, (preimage f (image f A1)) = A1 <-> exists A2, preimage f A2 = A1.
+Proof.
+intros A1; split.
+intros HA1; exists (image f A1); easy.
+intros [A2 HA2]; rewrite <- HA2; apply preimage_of_image_of_preimage.
+Qed.
+
+End Image_Preimage_Facts.
+
+
+Section Compose_Facts.
+
+(** Facts about composition of functions. *)
+
+Context {U1 U2 U3 U4 : Type}. (* Universes. *)
+
+Variable f12 : U1 -> U2. (* Function. *)
+Variable f23 : U2 -> U3. (* Function. *)
+Variable f34 : U3 -> U4. (* Function. *)
+
+(* Useful? *)
+Lemma compose_assoc :
+  compose f34 (compose f23 f12) = compose (compose f34 f23) f12.
+Proof.
+easy.
+Qed.
+
+Lemma image_compose :
+  forall A1, image (compose f23 f12) A1 = image f23 (image f12 A1).
+Proof.
+intros A1; apply subset_ext_equiv; split; intros x3 Hx3.
+induction Hx3 as [x1 Hx1]; easy.
+induction Hx3 as [x2 Hx2], Hx2 as [x1 Hx1].
+replace (f23 (f12 x1)) with (compose f23 f12 x1); easy.
+Qed.
+
+(* Useful? *)
+Lemma preimage_compose :
+  forall A3, preimage (compose f23 f12) A3 = preimage f12 (preimage f23 A3).
+Proof.
+easy.
+Qed.
+
+End Compose_Facts.

Lebesgue/Subset_any.v

+(**
+This file is part of the Elfic library
+
+Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
+
+This library is free software; you can redistribute it and/or
+modify it under the terms of the GNU Lesser General Public
+License as published by the Free Software Foundation; either
+version 3 of the License, or (at your option) any later version.
+
+This library is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+COPYING file for more details.
+*)
+
+(** Uncountable iterations of operators on subsets (definitions and properties).
+
+  Uncountable collections of subsets of type U are either represented
+  by functions of type Idx -> U -> Prop for some type of indices Idx, or
+  by subset systems of type (U -> Prop) -> Prop (ie subsets of the power set
+  of U).
+
+  Most of the properties are tautologies, and can be found on Wikipedia:
+  https://en.wikipedia.org/wiki/List_of_set_identities_and_relations
+
+  All or parts of this file could use BigOps from MathComp. *)
+
+From Coq Require Import Classical FunctionalExtensionality.
+
+Require Import Subset Subset_system_def.
+
+
+Section Any_Def.
+
+(** Implementation using an arbitrary index. *)
+
+Context {U U1 U2 : Type}. (* Universes. *)
+Context {Idx : Type}. (* Indices. *)
+
+Variable A B : Idx -> U -> Prop. (* Subset collections. *)
+
+Definition incl_any : Prop := forall i, incl (A i) (B i).
+Definition same_any : Prop := forall i, same (A i) (B i). (* Should it be A i = B i? *)
+
+Definition compl_any : Idx -> U -> Prop := fun i => compl (A i).
+
+Definition union_any : U -> Prop := fun x => exists i, A i x.
+Definition inter_any : U -> Prop := fun x => forall i, A i x.
+
+Variable A1 : Idx -> U1 -> Prop. (* Subset collection. *)
+Variable B2 : U2 -> Prop. (* Subset. *)
+Variable B1 : U1 -> Prop. (* Subset. *)
+Variable A2 : Idx -> U2 -> Prop. (* Subset collection. *)
+
+Definition prod_any_l : Idx -> U1 * U2 -> Prop := fun i => prod (A1 i) B2.
+Definition prod_any_r : Idx -> U1 * U2 -> Prop := fun i => prod B1 (A2 i).
+
+End Any_Def.
+
+
+Section Prop_Def.
+
+(** Implementation using a predicate. *)
+
+Context {U U1 U2 : Type}. (* Universes. *)
+
+Variable PA PB : (U -> Prop) -> Prop. (* Subset systems. *)
+
+Definition incl_Prop : Prop := Incl PA PB.
+Definition same_Prop : Prop := Same PA PB.
+
+Definition compl_Prop : (U -> Prop) -> Prop := fun A => PA (compl A).
+
+Definition union_Prop : U -> Prop := fun x => exists A, PA A /\ A x.
+Definition inter_Prop : U -> Prop := fun x => forall A, PA A -> A x.
+
+Variable P1 : (U1 -> Prop) -> Prop. (* Subset system. *)
+Variable B2 : U2 -> Prop. (* Subset. *)
+Variable B1 : U1 -> Prop. (* Subset. *)
+Variable P2 : (U2 -> Prop) -> Prop. (* Subset system. *)
+
+Inductive prod_Prop_l : (U1 * U2 -> Prop) -> Prop :=
+  | PPL : forall A1, P1 A1 -> prod_Prop_l (prod A1 B2).
+
+Inductive prod_Prop_r : (U1 * U2 -> Prop) -> Prop :=
+  | PPR : forall A2, P2 A2 -> prod_Prop_r (prod B1 A2).
+
+End Prop_Def.
+
+
+Section Any_Facts0.
+
+Context {U Idx : Type}.
+
+(** Extensionality of collections of subsets. *)
+
+Lemma subset_any_ext :
+  forall (A B : Idx -> U -> Prop),
+    same_any A B -> A = B.
+Proof.
+intros A B H; apply functional_extensionality; intros i.
+apply subset_ext, H.
+Qed.
+
+Lemma subset_any_ext_equiv :
+  forall (A B : Idx -> U -> Prop),
+    A = B <-> incl_any A B /\ incl_any B A.
+Proof.
+intros; split.
+intros H; split; now rewrite H.
+intros [H1 H2]; apply subset_any_ext; split; [apply H1 | apply H2].
+Qed.
+
+End Any_Facts0.
+
+
+Section Prop_Facts0.
+
+Context {U : Type}.
+
+(** Extensionality of collections of subsets. *)
+
+Lemma subset_Prop_ext :
+  forall (PA PB : (U -> Prop) -> Prop),
+    same_Prop PA PB -> PA = PB.
+Proof.
+exact Ext.
+Qed.
+
+Lemma subset_Prop_ext_equiv :
+  forall (PA PB : (U -> Prop) -> Prop),
+    PA = PB <-> incl_Prop PA PB /\ incl_Prop PB PA.
+Proof.
+exact Ext_equiv.
+Qed.
+
+End Prop_Facts0.
+
+
+Ltac subset_any_unfold :=
+  repeat unfold
+    same_any, incl_any, same_Prop, incl_Prop, (* Predicates. *)
+    prod_any_r, prod_any_l, inter_any, union_any, compl_any,
+    inter_Prop, union_Prop, compl_Prop. (* Operators. *)
+
+Ltac subset_any_full_unfold :=
+  subset_any_unfold; subset_unfold.
+
+Ltac subset_any_auto :=
+  subset_any_unfold; try easy; try tauto; auto.
+
+Ltac subset_any_full_auto :=
+  subset_any_unfold; subset_auto.
+
+
+Section Any_Facts.
+
+Context {U Idx : Type}. (* Universe. *)
+
+(** Facts about predicates on collections of subsets. *)
+
+(** incl_any is an order binary relation. *)
+
+Lemma incl_any_refl :
+  forall (A B : Idx -> U -> Prop),
+    same_any A B -> incl_any A B.
+Proof.
+intros A B H i; apply incl_refl; auto.
+Qed.
+
+Lemma incl_any_antisym :
+  forall (A B : Idx -> U -> Prop),
+    incl_any A B -> incl_any B A -> same_any A B.
+Proof.
+intros A B H1 H2.
+assert (HH : A = B -> same_any A B).
+  intros H'; now rewrite H'.
+now apply HH, subset_any_ext_equiv.
+Qed.
+
+Lemma incl_any_trans :
+  forall (A B C : Idx -> U -> Prop),
+    incl_any A B -> incl_any B C -> incl_any A C.
+Proof.
+intros A B C H1 H2 n x Hx; now apply H2, H1.
+Qed.
+
+(** same_any is an equivalence binary relation. *)
+
+(* Useless?
+Lemma same_any_refl :
+  forall (A : Idx -> U -> Prop),
+    same_any A A.
+Proof.
+easy.
+Qed.*)
+
+Lemma same_any_sym :
+  forall (A B : Idx -> U -> Prop),
+    same_any A B -> same_any B A.
+Proof.
+intros A B H n; apply same_sym, (H n).
+Qed.
+
+Lemma same_any_trans :
+  forall (A B C : Idx -> U -> Prop),
+    same_any A B -> same_any B C -> same_any A C.
+Proof.
+intros A B C H1 H2 n; apply same_trans with (B n).
+apply (H1 n).
+apply (H2 n).
+Qed.
+
+(** Facts about operations on collections of subsets. *)
+
+(** Facts about compl_any. *)
+
+Lemma compl_any_invol :
+  forall (A : Idx -> U -> Prop),
+    compl_any (compl_any A) = A.
+Proof.
+intros; apply subset_any_ext.
+intros i x; subset_any_full_auto.
+Qed.
+
+Lemma compl_any_monot :
+  forall (A B : Idx -> U -> Prop),
+    incl_any A B -> incl_any (compl_any B) (compl_any A).
+Proof.
+subset_any_unfold; intros; now apply compl_monot, H.
+Qed.
+
+Lemma incl_compl_any_equiv :
+  forall (A B : Idx -> U -> Prop),
+    incl_any A B <-> incl_any (compl_any B) (compl_any A).
+Proof.
+intros; split.
+apply compl_any_monot.
+rewrite <- (compl_any_invol A) at 2; rewrite <- (compl_any_invol B) at 2.
+apply compl_any_monot.
+Qed.
+
+Lemma same_compl_any :
+  forall (A B : Idx -> U -> Prop),
+    same_any A B -> same_any (compl_any A) (compl_any B).
+Proof.
+intros A B H i; apply same_compl, H.
+Qed.
+
+Lemma same_compl_any_equiv :
+  forall (A B : Idx -> U -> Prop),
+    same_any A B <-> same_any (compl_any A) (compl_any B).
+Proof.
+intros; split.
+apply same_compl_any.
+rewrite <- (compl_any_invol A) at 2; rewrite <- (compl_any_invol B) at 2.
+apply same_compl_any.
+Qed.
+
+Lemma compl_any_reg :
+  forall (A B : Idx -> U -> Prop),
+    same_any (compl_any A) (compl_any B) -> A = B.
+Proof.
+intros; now apply subset_any_ext, same_compl_any_equiv.
+Qed.
+
+(** Facts about union_any and inter_any. *)
+
+Lemma union_any_nullary :
+  ~ inhabited Idx ->
+  forall (A : Idx -> U -> Prop), union_any A = emptyset.
+Proof.
+intros H A; apply empty_emptyset; intros x [i Hx].
+apply H; easy.
+Qed.
+
+Lemma union_any_empty :
+  forall (A : Idx -> U -> Prop),
+    union_any A = emptyset <-> forall i, A i = emptyset.
+Proof.
+intros A; rewrite <- empty_emptyset; split; intros H.
+intros i; rewrite <- empty_emptyset; intros x Hx; apply (H x); now exists i.
+intros x [i Hx]; specialize (H i); rewrite <- empty_emptyset in H; now apply (H x).
+Qed.
+
+Lemma union_any_monot :
+  forall (A B : Idx -> U -> Prop),
+    incl_any A B ->
+    incl (union_any A) (union_any B).
+Proof.
+intros A B H x [i Hx]; exists i; now apply H.
+Qed.
+
+Lemma union_any_ub :
+  forall (A : Idx -> U -> Prop) i,
+    incl (A i) (union_any A).
+Proof.
+intros A i x Hx; now exists i.
+Qed.
+
+Lemma union_any_full :
+  forall (A : Idx -> U -> Prop),
+    (exists i, A i = fullset) ->
+    union_any A = fullset.
+Proof.
+intros A [i HAi].
+apply subset_ext_equiv; split; try easy.
+rewrite <- HAi; now apply union_any_ub.
+Qed.
+
+Lemma union_any_lub :
+  forall (A : Idx -> U -> Prop) (B : U -> Prop),
+    (forall i, incl (A i) B) ->
+    incl (union_any A) B.
+Proof.
+intros A B H x [i Hx]; now apply (H i).
+Qed.
+
+Lemma incl_union_any :
+  forall (A : Idx -> U -> Prop) (B : U -> Prop),
+    incl (union_any A) B ->
+    forall i, incl (A i) B.
+Proof.
+intros A B H i x Hx; apply H; now exists i.
+Qed.
+
+Lemma union_union_any_distr_l :
+  inhabited Idx ->
+  forall (A : U -> Prop) (B : Idx -> U -> Prop),
+    union A (union_any B) = union_any (fun i => union A (B i)).
+Proof.
+intros [i0] A B; apply subset_ext; intros x; split.
+intros [Hx | [i Hx]]; [exists i0; now left | exists i; now right].
+intros [i [Hx | Hx]]; [now left | right; now exists i].
+Qed.
+
+Lemma union_union_any_distr_r :
+  inhabited Idx ->
+  forall (A : Idx -> U -> Prop) (B : U -> Prop),
+    union (union_any A) B = union_any (fun i => union (A i) B).
+Proof.
+intros; rewrite union_comm, union_union_any_distr_l; try easy.
+f_equal; apply functional_extensionality; intros; apply union_comm.
+Qed.
+
+Lemma inter_union_any_distr_l :
+  forall (A : U -> Prop) (B : Idx -> U -> Prop),
+    inter A (union_any B) = union_any (fun i => inter A (B i)).
+Proof.
+intros A B; apply subset_ext; intros x; split.
+intros [Hx1 [i Hx2]]; now exists i.
+intros [i [Hx1 Hx2]]; split; [easy | now exists i].
+Qed.
+
+Lemma inter_union_any_distr_r :
+  forall (A : Idx -> U -> Prop) (B : U -> Prop),
+    inter (union_any A) B = union_any (fun i => inter (A i) B).
+Proof.
+intros; rewrite inter_comm, inter_union_any_distr_l.
+f_equal; apply functional_extensionality; intros; apply inter_comm.
+Qed.
+
+Lemma inter_any_nullary :
+  ~ inhabited Idx ->
+  forall (A : Idx -> U -> Prop), inter_any A = fullset.
+Proof.
+intros H A; apply (full_fullset (_ A)); intros x i.
+contradict H; easy.
+Qed.
+
+Lemma inter_any_full :
+  forall (A : Idx -> U -> Prop),
+    inter_any A = fullset <-> forall i, A i = fullset.
+Proof.
+intros A; rewrite <- full_fullset; split; intros H.
+intros i; rewrite <- full_fullset; intros x; now apply (H x).
+intros x i; specialize (H i); rewrite <- full_fullset in H; now apply (H x).
+Qed.
+
+Lemma inter_any_monot :
+  forall (A B : Idx -> U -> Prop),
+    incl_any A B ->
+    incl (inter_any A) (inter_any B).
+Proof.
+intros A B H x Hx i; apply H, Hx.
+Qed.
+
+Lemma inter_any_empty :
+  forall (A : Idx -> U -> Prop),
+    (exists i, A i = emptyset) ->
+    inter_any A = emptyset.
+Proof.
+intros A [i HAi].
+apply subset_ext_equiv; split; try easy.
+now rewrite <- HAi.
+Qed.
+
+Lemma inter_any_glb :
+  forall (A : Idx -> U -> Prop) (B : U -> Prop),
+    (forall i, incl B (A i)) ->
+    incl B (inter_any A).
+Proof.
+intros A B H x Hx i; now apply H.
+Qed.
+
+Lemma incl_inter_any :
+  forall (A : Idx -> U -> Prop) (B : U -> Prop),
+    incl B (inter_any A) ->
+    forall i, incl B (A i).
+Proof.
+intros A B H i x Hx; now apply H.
+Qed.
+
+Lemma union_inter_any_distr_l :
+  forall (A : U -> Prop) (B : Idx -> U -> Prop),
+    union A (inter_any B) = inter_any (fun i => union A (B i)).
+Proof.
+intros A B; apply subset_ext; intros x; split.
+intros [Hx | Hx] i; [now left | right; apply Hx].
+intros Hx1; case (classic (A x)); intros Hx2.
+now left.
+right; intros i; now destruct (Hx1 i).
+Qed.
+
+Lemma union_inter_any_distr_r :
+  forall (A : Idx -> U -> Prop) (B : U -> Prop),
+    union (inter_any A) B = inter_any (fun i => union (A i) B).
+Proof.
+intros; rewrite union_comm, union_inter_any_distr_l.
+f_equal; apply functional_extensionality; intros; apply union_comm.
+Qed.
+
+Lemma inter_inter_any_distr_l :
+  inhabited Idx ->
+  forall (A : U -> Prop) (B : Idx -> U -> Prop),
+    inter A (inter_any B) = inter_any (fun i => inter A (B i)).
+Proof.
+intros [i0] A B; apply subset_ext; intros x; split.
+intros [Hx1 Hx2] i; split; [easy | apply Hx2].
+intros Hx; split; [apply (Hx i0) | intros i; apply (Hx i)].
+Qed.
+
+Lemma inter_inter_any_distr_r :
+  inhabited Idx ->
+  forall (A : Idx -> U -> Prop) (B : U -> Prop),
+    inter (inter_any A) B = inter_any (fun i => inter (A i) B).
+Proof.
+intros; rewrite inter_comm, inter_inter_any_distr_l; try easy.
+f_equal; apply functional_extensionality; intros; apply inter_comm.
+Qed.
+
+(** De Morgan's laws. *)
+
+Lemma compl_union_any :
+  forall (A : Idx -> U -> Prop),
+    compl (union_any A) = inter_any (compl_any A).
+Proof.
+intros; apply subset_ext; split.
+intros H i Hx; apply H; now exists i.
+intros H [i Hx]; now apply (H i).
+Qed.
+
+Lemma compl_inter_any :
+  forall (A : Idx -> U -> Prop),
+    compl (inter_any A) = union_any (compl_any A).
+Proof.
+intros; apply compl_reg; rewrite compl_union_any.
+now rewrite compl_invol, compl_any_invol.
+Qed.
+
+Lemma compl_any_union_any :
+  forall (A : Idx -> U -> Prop)
+      (f : (Idx -> U -> Prop) -> Idx -> Idx -> U -> Prop),
+    (forall (A : Idx -> U -> Prop) i0,
+      compl_any (f A i0) = f (compl_any A) i0) ->
+    compl_any (fun i => union_any (f A i)) =
+      (fun i => inter_any (f (compl_any A) i)).
+Proof.
+intros A f Hf; apply subset_any_ext; intros i x; unfold compl_any.
+now rewrite compl_union_any, Hf.
+Qed.
+
+Lemma compl_any_inter_any :
+  forall (A : Idx -> U -> Prop)
+      (f : (Idx -> U -> Prop) -> Idx -> Idx -> U -> Prop),
+    (forall (A : Idx -> U -> Prop) i0,
+      compl_any (f A i0) = f (compl_any A) i0) ->
+    compl_any (fun i => inter_any (f A i)) =
+      (fun i => union_any (f (compl_any A) i)).
+Proof.
+intros A f Hf; apply subset_any_ext; intros i x; unfold compl_any.
+now rewrite compl_inter_any, Hf.
+Qed.
+
+(** ``Distributivity'' of diff. *)
+
+Lemma diff_union_any_distr_l :
+  forall (A : Idx -> U -> Prop) (B : U -> Prop),
+    diff (union_any A) B = union_any (fun i => diff (A i) B).
+Proof.
+intros; now rewrite diff_equiv_def_inter, inter_union_any_distr_r.
+Qed.
+
+Lemma diff_union_any_r :
+  inhabited Idx ->
+  forall (A : U -> Prop) (B : Idx -> U -> Prop),
+    diff A (union_any B) = inter_any (fun i => diff A (B i)).
+Proof.
+intros; now rewrite diff_equiv_def_inter, compl_union_any, inter_inter_any_distr_l.
+Qed.
+
+(* TODO: use another index type Jdx for B. *)
+Lemma diff_union_any :
+  inhabited Idx ->
+  forall (A B : Idx -> U -> Prop),
+    diff (union_any A) (union_any B) =
+    union_any (fun i => inter_any (fun j => diff (A i) (B j))).
+Proof.
+intros; rewrite diff_union_any_distr_l; f_equal.
+apply functional_extensionality; intros; now apply diff_union_any_r.
+Qed.
+
+Lemma diff_union_any_alt :
+  inhabited Idx ->
+  forall (A B : Idx -> U -> Prop),
+    diff (union_any A) (union_any B) =
+    inter_any (fun j => union_any (fun i => diff (A i) (B j))).
+Proof.
+intros; rewrite diff_union_any_r; try easy; f_equal.
+apply functional_extensionality; intros; apply diff_union_any_distr_l.
+Qed.
+
+Lemma diff_inter_any_distr_l :
+  inhabited Idx ->
+  forall (A : Idx -> U -> Prop) (B : U -> Prop),
+    diff (inter_any A) B = inter_any (fun i => diff (A i) B).
+Proof.
+intros; now rewrite diff_equiv_def_inter, inter_inter_any_distr_r.
+Qed.
+
+Lemma diff_inter_any_r :
+  forall (A : U -> Prop) (B : Idx -> U -> Prop),
+    diff A (inter_any B) = union_any (fun i => diff A (B i)).
+Proof.
+intros; now rewrite diff_equiv_def_inter, compl_inter_any, inter_union_any_distr_l.
+Qed.
+
+Lemma diff_inter_any :
+  inhabited Idx ->
+  forall (A B : Idx -> U -> Prop),
+    diff (inter_any A) (inter_any B) =
+    inter_any (fun i => union_any (fun j => diff (A i) (B j))).
+Proof.
+intros; rewrite diff_inter_any_distr_l; try easy; f_equal.
+apply functional_extensionality; intros; apply diff_inter_any_r.
+Qed.
+
+Lemma diff_inter_any_alt :
+  inhabited Idx ->
+  forall (A B : Idx -> U -> Prop),
+    diff (inter_any A) (inter_any B) =
+    union_any (fun j => inter_any (fun i => diff (A i) (B j))).
+Proof.
+intros; rewrite diff_inter_any_r; f_equal.
+apply functional_extensionality; intros; now apply diff_inter_any_distr_l.
+Qed.
+
+Lemma diff_union_inter_any :
+  forall (A B : Idx -> U -> Prop),
+    diff (union_any A) (inter_any B) =
+    union_any (fun i => union_any (fun j => diff (A i) (B j))).
+Proof.
+intros; rewrite diff_union_any_distr_l; f_equal.
+apply functional_extensionality; intros; apply diff_inter_any_r.
+Qed.
+
+Lemma diff_union_inter_any_alt :
+  forall (A B : Idx -> U -> Prop),
+    diff (union_any A) (inter_any B) =
+    union_any (fun j => union_any (fun i => diff (A i) (B j))).
+Proof.
+intros; rewrite diff_inter_any_r; f_equal.
+apply functional_extensionality; intros; apply diff_union_any_distr_l.
+Qed.
+
+Lemma diff_inter_union_any :
+  inhabited Idx ->
+  forall (A B : Idx -> U -> Prop),
+    diff (inter_any A) (union_any B) =
+    inter_any (fun i => inter_any (fun j => diff (A i) (B j))).
+Proof.
+intros; rewrite diff_inter_any_distr_l; try easy; f_equal.
+apply functional_extensionality; intros; now apply diff_union_any_r.
+Qed.
+
+Lemma diff_inter_union_any_alt :
+  inhabited Idx ->
+  forall (A B : Idx -> U -> Prop),
+    diff (inter_any A) (union_any B) =
+    inter_any (fun j => inter_any (fun i => diff (A i) (B j))).
+Proof.
+intros; rewrite diff_union_any_r; try easy; f_equal.
+apply functional_extensionality; intros; now apply diff_inter_any_distr_l.
+Qed.
+
+End Any_Facts.
+
+
+Section Prod_Facts.
+
+(** Facts about Cartesian product. *)
+
+Context {U1 U2 Idx : Type}. (* Universes. *)
+
+Lemma prod_union_any_full :
+  forall (A1 : Idx -> U1 -> Prop),
+    prod (union_any A1) (@fullset U2) =
+      union_any (prod_any_l A1 fullset).
+Proof.
+intros; apply subset_ext; subset_any_full_unfold.
+intros A; split.
+intros [[i HA] _]; now exists i.
+intros [i [HA _]]; split; now try exists i.
+Qed.
+
+Lemma prod_full_union_any :
+  forall (A2 : Idx -> U2 -> Prop),
+    prod (@fullset U1) (union_any A2) =
+      union_any (prod_any_r fullset A2).
+Proof.
+intros; apply subset_ext; subset_any_full_unfold.
+intros A; split.
+intros [_ [i HA]]; now exists i.
+intros [i [_ HA]]; split; now try exists i.
+Qed.
+
+Lemma prod_inter_any_full :
+  forall (A1 : Idx -> U1 -> Prop),
+    prod (inter_any A1) (@fullset U2) =
+      inter_any (prod_any_l A1 fullset).
+Proof.
+intros; apply subset_ext; subset_any_full_unfold.
+intros A; split.
+intros [HA _] i; split; now try apply (HA i).
+intros HA; split; try easy; apply HA.
+Qed.
+
+Lemma prod_full_inter_any :
+  forall (A2 : Idx -> U2 -> Prop),
+    prod (@fullset U1) (inter_any A2) =
+      inter_any (prod_any_r fullset A2).
+Proof.
+intros; apply subset_ext; subset_any_full_unfold.
+intros A; split.
+intros [_ HA] i; split; now try apply (HA i).
+intros HA; split; try easy; apply HA.
+Qed.
+
+End Prod_Facts.

Lebesgue/Subset_system_def.v

+(**
+This file is part of the Elfic library
+
+Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
+
+This library is free software; you can redistribute it and/or
+modify it under the terms of the GNU Lesser General Public
+License as published by the Free Software Foundation; either
+version 3 of the License, or (at your option) any later version.
+
+This library is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+COPYING file for more details.
+*)
+
+Require Import Subset.
+
+
+Section Subset_system_Prop_Def.
+
+Context {U : Type}. (* Universe. *)
+
+Variable P Q : (U -> Prop) -> Prop. (* Subset systems. *)
+
+Definition Incl : Prop := @incl (U -> Prop) P Q.
+
+Definition Same : Prop := @same (U -> Prop) P Q.
+
+End Subset_system_Prop_Def.
+
+
+Section Subset_system_Prop.
+
+Context {U : Type}. (* Universe. *)
+
+(** Extensionality of systems of subsets. *)
+
+Lemma Ext :
+  forall (P Q : (U -> Prop) -> Prop),
+    Same P Q -> P = Q.
+Proof.
+exact (@subset_ext (U -> Prop)).
+Qed.
+
+Lemma Ext_equiv :
+  forall (P Q : (U -> Prop) -> Prop),
+    P = Q <-> Incl P Q /\ Incl Q P.
+Proof.
+exact (@subset_ext_equiv (U -> Prop)).
+Qed.
+
+(** Incl is an order binary relation. *)
+
+Lemma Incl_refl :
+  forall (P Q : (U -> Prop) -> Prop),
+    Same P Q -> Incl P Q.
+Proof.
+exact (@incl_refl (U -> Prop)).
+Qed.
+
+Lemma Incl_antisym :
+  forall (P Q : (U -> Prop) -> Prop),
+    Incl P Q -> Incl Q P -> P = Q.
+Proof.
+exact (@incl_antisym (U -> Prop)).
+Qed.
+
+Lemma Incl_trans :
+  forall (P Q R : (U -> Prop) -> Prop),
+    Incl P Q -> Incl Q R -> Incl P R.
+Proof.
+exact (@incl_trans (U -> Prop)).
+Qed.
+
+(** Same is an equivalence binary relation. *)
+
+(* Useless?
+Lemma Same_refl :
+  forall (P : (U -> Prop) -> Prop),
+    Same P P.
+Proof.
+easy.
+Qed.*)
+
+Lemma Same_sym :
+  forall (P Q : (U -> Prop) -> Prop),
+    Same P Q -> Same Q P.
+Proof.
+exact (@same_sym (U -> Prop)).
+Qed.
+
+Lemma Same_trans :
+  forall (P Q R : (U -> Prop) -> Prop),
+    Same P Q -> Same Q R -> Same P R.
+Proof.
+exact (@same_trans (U -> Prop)).
+Qed.
+
+End Subset_system_Prop.

Lebesgue/Topology.v

+(**
+This file is part of the Elfic library
+
+Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
+
+This library is free software; you can redistribute it and/or
+modify it under the terms of the GNU Lesser General Public
+License as published by the Free Software Foundation; either
+version 3 of the License, or (at your option) any later version.
+
+This library is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+COPYING file for more details.
+*)
+
+(** General topology (definitions and properties). *)
+
+From Coquelicot Require Import Coquelicot.
+
+Require Import UniformSpace_compl.
+Require Import Subset.
+
+
+Section topo_basis_Facts1.
+
+Context {T T1 T2 : UniformSpace}.
+
+Lemma is_topo_basis_Prop_open : is_topo_basis_Prop (@open T).
+Proof.
+split; try easy.
+intros A HA x; split.
+intros Hx; exists A; easy.
+intros [B [[HB1 HB2] HB3]]; auto.
+Qed.
+
+Lemma is_topo_basis_to_Prop :
+  forall Idx (B : Idx -> T -> Prop),
+    is_topo_basis B -> is_topo_basis_Prop (subset_of_Idx B).
+Proof.
+intros Idx B [HB1 HB2]; split.
+intros B' [i HB']; rewrite HB'; auto.
+intros A HA x; destruct (HB2 A HA) as [P HP]; rewrite HP; split.
+(* *)
+intros [i [Hi Hx]]; exists (B i); repeat split; try exists i; try easy.
+intros y Hy; apply <- HP; exists i; easy.
+(* *)
+intros [B' [[[i HB'1] HB'2] HB'3]].
+destruct (proj1 (HP x) (HB'2 x HB'3)) as [j Hj]; exists j; easy.
+Qed.
+
+Lemma is_topo_basis_of_Prop :
+  forall (PB : (T -> Prop) -> Prop),
+    is_topo_basis_Prop PB -> is_topo_basis (subset_to_Idx PB).
+Proof.
+intros PB [HPB1 HPB2]; split.
+intros i; apply HPB1, subset_to_Idx_correct; exists i; easy.
+intros A HA; exists (fun i => forall y, subset_to_Idx PB i y -> A y); intros x.
+rewrite (HPB2 _ HA); split.
+(* *)
+intros [B' [[HB'1 HB'2] HB'3]].
+destruct (proj1 (subset_to_Idx_correct PB B') HB'1) as [i Hi]; rewrite Hi in *.
+exists i; easy.
+(* *)
+intros [i [Hi1 Hi2]].
+exists (subset_to_Idx PB i); repeat split; try easy.
+apply subset_to_Idx_correct; exists i; easy.
+Qed.
+
+Lemma open_compat_is_topo_basis_compat :
+  forall (f : T1 -> T2) (P2 : (T2 -> Prop) -> Prop),
+    is_topo_basis_Prop P2 ->
+    (forall A2, open A2 -> open (fun x1 => A2 (f x1))) ->
+    forall B2, P2 B2 -> open (fun x1 => B2 (f x1)).
+Proof.
+intros f P2 [HP2 _]; auto.
+Qed.
+
+End topo_basis_Facts1.
+
+
+Section topo_basis_Facts2.
+
+Context {T1 T2 : UniformSpace}.
+
+Variable f : T1 -> T2.
+
+Lemma topo_basis_compat_is_continuous :
+  forall (P2 : (T2 -> Prop) -> Prop),
+    is_topo_basis_Prop P2 ->
+    (forall B2, P2 B2 -> open (fun x1 => B2 (f x1))) ->
+    forall x1, continuous f x1.
+Proof.
+intros P2 HP2 Hf x1.
+
+
+
+
+
+Admitted.
+
+Lemma continuous_equiv_open :
+  (forall x1, continuous f x1) <->
+  (forall A2, open A2 -> open (fun x1 => A2 (f x1))).
+Proof.
+intros; split.
+apply continuous_is_open_compat.
+intro; apply topo_basis_compat_is_continuous with (P2 := open); try easy.
+apply is_topo_basis_Prop_open.
+Qed.
+
+Lemma continuous_equiv_closed :
+  (forall x1, continuous f x1) <->
+  (forall A2, closed A2 -> closed (fun x1 => A2 (f x1))).
+Proof.
+rewrite continuous_equiv_open; split; intros Hf A2 HA2.
+(* *)
+
+
+
+
+
+Admitted.
+
+End topo_basis_Facts2.

Lebesgue/_CoqProject

@@ -24,14 +24,22 @@ Subset.v
 Subset_dec.v
 Subset_charac.v
 Subset_finite.v
+
+Subset_system_def.v
+Subset_any.v
 Subset_seq.v
-Subset_R.v
-Subset_Rbar.v
+
+Function.v
 
 Subset_system_base.v
 Subset_system_gen.v
 Subset_system.v
 
+Topology.v
+
+Subset_R.v
+Subset_Rbar.v
+
 measurable.v
 measurable_R.v
 measurable_Rbar.v