Add image/preimage.

WIP: many facts about image/preimage.

Lebesgue/Subset.v

@@ -19,7 +19,7 @@ COPYING file for more details.
   Subsets of the type U are represented by their belonging function,
   of type U -> Prop.
 
-  Most of the properties are tautologies that can be found on Wikipedia:
+  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 Classical.
@@ -132,6 +132,23 @@ Definition swap : forall {U : Type}, (U1 * U2 -> U) -> U2 * U1 -> U :=
 End Base_Def4.
 
 
+Section Base_Def5.
+
+Context {U1 U2 : Type}. (* Universes. *)
+
+Variable f : U1 -> U2. (* Function. *)
+Variable A1 : U1 -> Prop. (* Subset. *)
+Variable A2 : U2 -> Prop. (* Subset. *)
+
+Definition image : U2 -> Prop :=
+  fun x2 => exists x1, A1 x1 /\ x2 = f x1.
+
+Definition preimage : U1 -> Prop :=
+  fun x1 => A2 (f x1).
+
+End Base_Def5.
+
+
 Section Prop_Facts0.
 
 Context {U : Type}. (* Universe. *)
@@ -162,7 +179,7 @@ End Prop_Facts0.
 Ltac subset_unfold :=
   repeat unfold
     partition, disj, same, incl, full, nonempty, empty, (* Predicates. *)
-    pair, (* Constructor. *)
+    preimage, image, pair, (* Constructors. *)
     swap, prod, sym_diff, diff, add, inter, union, compl, (* Operators. *)
     singleton, Prop_cst, fullset, emptyset. (* Constructors. *)
 
@@ -574,18 +591,25 @@ Proof.
 intros A B; rewrite union_comm; apply union_left.
 Qed.
 
+Lemma union_monot :
+  forall (A B C D : U -> Prop),
+    incl A B -> incl C D -> incl (union A C) (union B D).
+Proof.
+intros A B C D HAB HCD x [Hx | Hx]; [left | right]; auto.
+Qed.
+
 Lemma union_monot_l :
   forall (A B C : U -> Prop),
     incl A B -> incl (union C A) (union C B).
 Proof.
-intros A B C H x [Hx | Hx]; [now left | right; now apply H].
+intros; apply union_monot; easy.
 Qed.
 
 Lemma union_monot_r :
   forall (A B C : U -> Prop),
     incl A B -> incl (union A C) (union B C).
 Proof.
-intros; rewrite (union_comm A), (union_comm B); now apply union_monot_l.
+intros; apply union_monot; easy.
 Qed.
 
 Lemma disj_union_l :
@@ -734,18 +758,25 @@ Proof.
 intros; rewrite inter_comm; apply inter_left.
 Qed.
 
+Lemma inter_monot :
+  forall (A B C D : U -> Prop),
+    incl A B -> incl C D -> incl (inter A C) (inter B D).
+Proof.
+intros A B C D HAB HCD x [Hx1 Hx2]; split; auto.
+Qed.
+
 Lemma inter_monot_l :
   forall (A B C : U -> Prop),
     incl A B -> incl (inter C A) (inter C B).
 Proof.
-intros A B C H x [Hx1 Hx2]; split; [easy | now apply H].
+intros; apply inter_monot; easy.
 Qed.
 
 Lemma inter_monot_r :
   forall (A B C : U -> Prop),
     incl A B -> incl (inter A C) (inter B C).
 Proof.
-intros; rewrite (inter_comm A), (inter_comm B); now apply inter_monot_l.
+intros; apply inter_monot; easy.
 Qed.
 
 Lemma disj_inter_l :
@@ -1764,3 +1795,192 @@ intros; subset_ext_auto.
 Qed.
 
 End Prod_Facts.
+
+
+Section Image_Facts.
+
+(** Facts about images. *)
+
+Context {U1 U2 : Type}. (* Universes. *)
+
+Variable f : U1 -> U2. (* Function. *)
+
+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)); exists 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].
+exists x1; split; try easy; apply H1; easy.
+Qed.
+
+Lemma image_compl : forall A1, incl (compl (image f A1)) (image f (compl A1)).
+Proof.
+intros y.
+Admitted.
+
+Lemma image_union :
+  forall A1 B1, image f (union A1 B1) = union (image f A1) (image f B1).
+Proof.
+Admitted.
+
+Lemma image_inter :
+  forall A1 B1, incl (image f (inter A1 B1)) (inter (image f A1) (image f B1)).
+Proof.
+Admitted.
+
+Lemma image_diff :
+  forall A1 B1, incl (diff (image f A1) (image f B1)) (image f (diff A1 B1)).
+Proof.
+Admitted.
+
+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.
+
+End Image_Facts.
+
+
+Section Preimage_Facts.
+
+(** Facts about preimages. *)
+
+Context {U1 U2 : Type}. (* Universes. *)
+
+Variable f : U1 -> U2. (* Function. *)
+
+Lemma preimage_empty_equiv :
+  forall A2, empty (preimage f A2) <-> disj A2 (image f fullset).
+Proof.
+Admitted.
+
+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]]; rewrite Hx1; specialize (HA2 x1); easy.
+intros x1; apply HA2; exists x1; easy.
+Qed.
+
+Lemma preimage_monot :
+  forall A2 B2, incl A2 B2 -> incl (preimage f A2) (preimage f B2).
+Proof.
+intros; subset_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.
+
+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 [x1 [Hx1a Hx1b]]; split.
+rewrite Hx1b; easy.
+exists x1; easy.
+(* *)
+intros [Hx2 [x1 [_ Hx1]]]; rewrite Hx1 in Hx2.
+exists x1; 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 subset_ext; intros x2; split.
+intros [Hx2 _]; easy.
+intros [x1 Hx1]; split; exists x1; easy.
+Qed.
+
+Lemma preimage_of_image : forall A1, incl A1 (preimage f (image f A1)).
+Proof.
+intros A1 x1 Hx1; exists x1; easy.
+Qed.
+
+Lemma preimage_of_image_full : preimage f (image f fullset) = fullset.
+Proof.
+apply subset_ext_equiv; split; try easy.
+apply preimage_of_image.
+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.

Lebesgue/Subset_finite.v

@@ -1409,3 +1409,51 @@ intros HA; split; now try apply HA.
 Qed.
 
 End Prod_Facts.
+
+
+Section Image_Facts.
+
+(** Facts about images. *)
+
+Context {U1 U2 : Type}. (* Universes. *)
+
+Variable f : U1 -> U2. (* Function. *)
+
+Lemma image_union_finite :
+  forall A1 N,
+    image f (union_finite A1 N) = union_finite (fun n => image f (A1 n)) N.
+Proof.
+Admitted.
+
+Lemma image_inter_finite :
+  forall A1 N,
+    incl (image f (inter_finite A1 N)) (inter_finite (fun n => image f (A1 n)) N).
+Proof.
+Admitted.
+
+End Image_Facts.
+
+
+Section Preimage_Facts.
+
+(** Facts about preimages. *)
+
+Context {U1 U2 : Type}. (* Universes. *)
+
+Variable f : U1 -> U2. (* Function. *)
+
+Lemma preimage_union_finite :
+  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 :
+  forall A2 N,
+    preimage f (inter_finite A2 N) = inter_finite (fun n => preimage f (A2 n)) N.
+Proof.
+intros; subset_ext_auto.
+Qed.
+
+End Preimage_Facts.

Lebesgue/Subset_seq.v

@@ -1137,6 +1137,53 @@ Qed.
 End Prod_Facts.
 
 
+Section Image_Facts.
+
+(** Facts about images. *)
+
+Context {U1 U2 : Type}. (* Universes. *)
+
+Variable f : U1 -> U2. (* Function. *)
+
+Lemma image_union_seq :
+  forall A1, image f (union_seq A1) = union_seq (fun n => image f (A1 n)).
+Proof.
+Admitted.
+
+Lemma image_inter_seq :
+  forall A1,
+    incl (image f (inter_seq A1)) (inter_seq (fun n => image f (A1 n))).
+Proof.
+Admitted.
+
+End Image_Facts.
+
+
+Section Preimage_Facts.
+
+(** Facts about preimages. *)
+
+Context {U1 U2 : Type}. (* Universes. *)
+
+Variable f : U1 -> U2. (* Function. *)
+
+Lemma preimage_union_seq :
+  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 :
+  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 Limit_Def.
 
 Context {U : Type}. (* Universe. *)