Merge pull request #719 from IshiguroYoshihiro/subset_refl

subset_refl
math-comp · Aug 2, 2022 · 73bca8d · 73bca8d
2 parents 89dc746 + 8fc8c5b
commit 73bca8d
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 0 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -39,6 +39,8 @@
   + lemmas `bigmax_le` and `bigmax_lt`
   + lemma `bigmin_idr`
   + lemma `bigmax_idr`
+- in `classical_sets.v`:
+  + lemma `subset_refl`
 
 ### Changed
 

diff --git a/theories/classical_sets.v b/theories/classical_sets.v
@@ -485,6 +485,8 @@ Proof. by apply/seteqP; split=> x/=; rewrite inE. Qed.
 Lemma mem_setE (P : pred T) : mem [set` P] = mem P.
 Proof. by congr Mem; apply/funext=> x; apply/asboolP/idP. Qed.
 
+Lemma subset_refl A : A `<=` A. Proof. by []. Qed.
+
 Lemma subset_trans B A C : A `<=` B -> B `<=` C -> A `<=` C.
 Proof. by move=> sAB sBC ? ?; apply/sBC/sAB. Qed.