From a9f5e7dfbeaf3094db80c2ab523f4d10a57b4622 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Cl=C3=A9ment?= <francois.clement@inria.fr>
Date: Thu, 30 Jun 2022 11:26:39 +0200
Subject: [PATCH] Add monotony of {Inter,Union}_any_closure.
---
.../Set_theory/Set_system/Set_system_base_any.v | 14 ++++++++++++++
1 file changed, 14 insertions(+)
diff --git a/Lebesgue/Set_theory/Set_system/Set_system_base_any.v b/Lebesgue/Set_theory/Set_system/Set_system_base_any.v
index 7eb6f1b1..9977d75f 100644
--- a/Lebesgue/Set_theory/Set_system/Set_system_base_any.v
+++ b/Lebesgue/Set_theory/Set_system/Set_system_base_any.v
@@ -175,6 +175,20 @@ Section Any_Facts2.
Context {U : Type}.
+Lemma Inter_any_closure_monot :
+ forall (P1 P2 : set_system U),
+ Incl P1 P2 -> Incl (Inter_any_closure P1) (Inter_any_closure P2).
+Proof.
+intros P1 P2 HP A [Q1 HQ1]; apply Iac, Incl_trans with P1; easy.
+Qed.
+
+Lemma Union_any_closure_monot :
+ forall (P1 P2 : set_system U),
+ Incl P1 P2 -> Incl (Union_any_closure P1) (Union_any_closure P2).
+Proof.
+intros P1 P2 HP A [Q1 HQ1]; apply Uac, Incl_trans with P1; easy.
+Qed.
+
Lemma Inter_any_closure_complp_any_eq :
forall (P : set_system U),
Inter_any_closure (complp_any P) = complp_any (Union_any_closure P).
--
GitLab