From 5b648771aa0d03f2c8c2a20343e101570e078abf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr> Date: Tue, 21 Jun 2022 10:32:33 +0200 Subject: [PATCH] Rm wrong Lift_Trace_is_Subset_rev. Go for functional equalities. --- .../Set_system/Set_system_base_base.v | 26 +++++-------------- 1 file changed, 6 insertions(+), 20 deletions(-) diff --git a/Lebesgue/Set_theory/Set_system/Set_system_base_base.v b/Lebesgue/Set_theory/Set_system/Set_system_base_base.v index 40c779ae..d49d9d16 100644 --- a/Lebesgue/Set_theory/Set_system/Set_system_base_base.v +++ b/Lebesgue/Set_theory/Set_system/Set_system_base_base.v @@ -376,23 +376,9 @@ induction HB as [P B HB1 HB2]. apply inter_right in HB2; rewrite <- HB2; easy. Qed. -Lemma Lift_Trace_is_Subset_rev : - forall (P : set_system U), - Union_seq P -> compose (Lift A) (Trace A) P = Subset A P -> P A. -Proof. -intros P HP1; rewrite Lift_Trace; setp_any_unfold; intros HP2'. -assert (HP2 : forall B, image (inter A) P B <-> P B /\ incl B A). - intros; rewrite <- Subset_equiv, <- HP2'; easy. -clear HP2'. - - - -Admitted. - -Lemma Trace_Lift : forall (PA : subset_system A), Trace A (Lift A PA) = PA. +Lemma Trace_Lift : compose (Trace A) (Lift A) = id. Proof. -intros PA; unfold Trace, tracep_any, Lift, liftp_any. -rewrite <- image_compose, trace_lift; apply image_id. +rewrite <- image_id, <- trace_lift, image_compose; easy. Qed. Lemma Trace_monot: @@ -401,13 +387,13 @@ Proof. intros P1 P2 HP BA [B HB]; apply Im; auto. Qed. -Lemma Trace_Lift_full : forall (PA : subset_system A), Trace A (Lift_full A PA) = PA. +Lemma Trace_Lift_full : compose (Trace A) (Lift_full A) = id. Proof. -intros PA; apply Ext_equiv; split; intros BA HBA. +apply fun_ext; intros PA; apply Ext_equiv; split; intros BA HBA. induction HBA as [B HB]; easy. apply Trace_monot with (Lift A PA). apply Lift_Lift_full. -rewrite Trace_Lift; easy. +rewrite <- compose_eq, Trace_Lift; easy. Qed. Lemma Trace_equiv : forall (P : set_system U) B, Trace A P B <-> exists C, P C /\ B = trace A C. @@ -493,7 +479,7 @@ Lemma Preimage_compose : Proof. intros P3; unfold Preimage; set_ext_auto A1 HA1; induction HA1 as [A3 HA3]. rewrite preimage_compose; repeat apply Im; easy. -induction HA3 as [A3 HA3]; unfold preimagep_any; rewrite preimage_compose_fun. +induction HA3 as [A3 HA3]; unfold preimagep_any; rewrite preimage_compose. apply Im with (f := fun A => preimage f21 (preimage f32 A)); easy. Qed. -- GitLab