Library Lebesgue.Subset_system_def
This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
Definitions for subset systems.
Brief description
From Subsets Require Import Subsets.
Section Subset_system_Prop_Def.
Context {U : Type}.
Variable P Q : (U → Prop) → Prop.
Definition Incl : Prop := @incl (U → Prop) P Q.
Definition Same : Prop := @same (U → Prop) P Q.
End Subset_system_Prop_Def.
Section Subset_system_Prop.
Context {U : Type}.
Extensionality of systems of subsets.
Lemma Ext :
∀ (P Q : (U → Prop) → Prop),
Same P Q → P = Q.
Proof.
exact (@subset_ext (U → Prop)).
Qed.
Lemma Ext_equiv :
∀ (P Q : (U → Prop) → Prop),
P = Q ↔ Incl P Q ∧ Incl Q P.
Proof.
exact (@subset_ext_equiv (U → Prop)).
Qed.
Incl is an order binary relation.
Lemma Incl_refl :
∀ (P Q : (U → Prop) → Prop),
Same P Q → Incl P Q.
Proof.
exact (@incl_refl (U → Prop)).
Qed.
Lemma Incl_antisym :
∀ (P Q : (U → Prop) → Prop),
Incl P Q → Incl Q P → P = Q.
Proof.
exact (@incl_antisym (U → Prop)).
Qed.
Lemma Incl_trans :
∀ (P Q R : (U → Prop) → Prop),
Incl P Q → Incl Q R → Incl P R.
Proof.
exact (@incl_trans (U → Prop)).
Qed.
Same is an equivalence binary relation.