From e08e68bbc304c5028007e76e818b44e6a69f0337 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Wed, 9 Aug 2023 10:10:11 -0600 Subject: [PATCH] Enderton. Fix lemma 3B header. --- Bookshelf/Enderton/Set/Chapter_3.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Bookshelf/Enderton/Set/Chapter_3.lean b/Bookshelf/Enderton/Set/Chapter_3.lean index 5312990..bcb908f 100644 --- a/Bookshelf/Enderton/Set/Chapter_3.lean +++ b/Bookshelf/Enderton/Set/Chapter_3.lean @@ -15,7 +15,7 @@ Relations and Functions namespace Enderton.Set.Chapter_3 -/-- #### Theorem 3B +/-- #### Lemma 3B If `x ∈ C` and `y ∈ C`, then `⟨x, y⟩ ∈ 𝒫 𝒫 C`. -/