From 8d877d940496190da1b2480bc84b54a2263564c3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Mon, 20 Jun 2022 12:39:48 +0200
Subject: [PATCH] Add lemmas about id.
---
Lebesgue/Set_theory/Set_base.v | 7 +++++++
Lebesgue/Set_theory/Set_fun.v | 18 ++++++++++++++++--
2 files changed, 23 insertions(+), 2 deletions(-)
diff --git a/Lebesgue/Set_theory/Set_base.v b/Lebesgue/Set_theory/Set_base.v
index 03c4470e..c22db4ca 100644
--- a/Lebesgue/Set_theory/Set_base.v
+++ b/Lebesgue/Set_theory/Set_base.v
@@ -2491,6 +2491,13 @@ Variable f : U1 -> U2.
(** Facts about image. *)
+Lemma image_id : forall {U : Type} (A : set U), image id A = A.
+Proof.
+intros; apply set_ext_equiv; split; intros x Hx.
+induction Hx as [x Hx]; easy.
+rewrite <- id_eq; easy.
+Qed.
+
Lemma image_empty_equiv :
forall A1, empty (image f A1) <-> empty A1.
Proof.
diff --git a/Lebesgue/Set_theory/Set_fun.v b/Lebesgue/Set_theory/Set_fun.v
index 52cf017c..d06e318f 100644
--- a/Lebesgue/Set_theory/Set_fun.v
+++ b/Lebesgue/Set_theory/Set_fun.v
@@ -21,7 +21,20 @@ From Coq Require Import ClassicalChoice.
Require Import Set_def.
-Section Fun_Facts0.
+Section Fun_Facts0a.
+
+Context {U : Type}.
+
+(* Useful? *)
+Lemma id_eq: forall (x : U), id x = x.
+Proof.
+easy.
+Qed.
+
+End Fun_Facts0a.
+
+
+Section Fun_Facts0b.
Context {U1 U2 : Type}.
@@ -53,7 +66,7 @@ Proof.
intros f g h H1 H2 x; now rewrite (H1 x).
Qed.
-End Fun_Facts0.
+End Fun_Facts0b.
Section Fun_Facts1.
@@ -110,6 +123,7 @@ Variable f43 : U3 -> U4.
Variable f32 : U2 -> U3.
Variable f21 : U1 -> U2.
+(* Useful? *)
Lemma compose_eq : forall (x1 : U1), compose f32 f21 x1 = f32 (f21 x1).
Proof.
easy.
--
GitLab