From 53ad437dab6fa2e5f839a9ccacbe664f22e0bba8 Mon Sep 17 00:00:00 2001 From: Dan Abramov Date: Mon, 28 Jul 2025 21:04:00 +0100 Subject: [PATCH] Add helper lemma for 3.4.7 --- analysis/Analysis/Section_3_4.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/analysis/Analysis/Section_3_4.lean b/analysis/Analysis/Section_3_4.lean index 1a5189196..26eca6677 100644 --- a/analysis/Analysis/Section_3_4.lean +++ b/analysis/Analysis/Section_3_4.lean @@ -391,6 +391,12 @@ theorem SetTheory.Set.image_preimage_of_surj {X Y:Set} (f:X → Y) : theorem SetTheory.Set.preimage_image_of_inj {X Y:Set} (f:X → Y) : (∀ S, S ⊆ X → preimage f (image f S) = S) ↔ Function.Injective f := by sorry +/-- Helper lemma for Exercise 3.4.7. -/ +@[simp] +lemma SetTheory.Set.mem_powerset' {S S' : Set} : (S': Object) ∈ S.powerset ↔ S' ⊆ S := by + rw [mem_powerset] + simp + /-- Exercise 3.4.7 -/ theorem SetTheory.Set.partial_functions {X Y:Set} : ∃ Z:Set, ∀ F:Object, F ∈ Z ↔ ∃ X' Y':Set, X' ⊆ X ∧ Y' ⊆ Y ∧ ∃ f: X' → Y', F = f := by