Proofs of image_diff, image_compl and preimage_empty_equiv.

Lebesgue/Subset.v

@@ -1825,17 +1825,6 @@ 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.
-subset_unfold; intros A1 x2 Hx2.
-(*apply not_ex_all_not in Hx2.*)
-
-
-
-
-
-Admitted.
-
 Lemma image_union :
   forall A1 B1, image f (union A1 B1) = union (image f A1) (image f B1).
 Proof.
@@ -1854,16 +1843,19 @@ Qed.
 Lemma image_diff :
   forall A1 B1, incl (diff (image f A1) (image f B1)) (image f (diff A1 B1)).
 Proof.
-intros; unfold diff.
-apply incl_trans with (inter (image f A1) (image f (compl B1))).
-apply inter_monot_l, image_compl.
-(*apply image_inter.*)
-
-
-
-
+intros A1 B1 x2 [[x1 Hx1] Hx2'].
+unfold compl, image in Hx2'.
+(*apply not_ex_all_not in Hx2. does not work! *)
+assert (Hx2 : forall x1, ~ B1 x1 \/ x2 <> f x1).
+  intros y1; apply not_and_or; generalize y1; apply not_ex_all_not; easy.
+clear Hx2'.
+exists x1; repeat split; try easy; destruct (Hx2 x1); easy.
+Qed.
 
-Admitted.
+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,
@@ -1887,7 +1879,10 @@ Variable f : U1 -> U2. (* Function. *)
 Lemma preimage_empty_equiv :
   forall A2, empty (preimage f A2) <-> disj A2 (image f fullset).
 Proof.
-Admitted.
+intros A2; split.
+intros HA2 x2 Hx2 [x1 [_ Hx1]]; apply (HA2 x1); rewrite Hx1 in Hx2; easy.
+intros HA2 x1 Hx1; apply (HA2(f x1)); try easy; exists x1; easy.
+Qed.
 
 Lemma preimage_emptyset : preimage f emptyset = emptyset.
 Proof.