From 28d3e87199c9d7fa5bd7811eb384b301c5d82460 Mon Sep 17 00:00:00 2001 From: Rado Kirov Date: Sun, 15 Mar 2026 22:54:39 -0700 Subject: [PATCH] Fix Section 8.4: unused variable warnings and missing sorry MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Replace unused `f` with `_` in `Function.equiv` left_inv/right_inv - Replace direct proof of `axiom_of_choice_from_exists_function` with `sorry` — the exercise asks to derive it from `exists_function`, so the proof should be left to the reader Co-Authored-By: Claude Opus 4.6 --- analysis/Analysis/Section_8_4.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/analysis/Analysis/Section_8_4.lean b/analysis/Analysis/Section_8_4.lean index 14625348..a26cf69b 100644 --- a/analysis/Analysis/Section_8_4.lean +++ b/analysis/Analysis/Section_8_4.lean @@ -52,8 +52,8 @@ def CartesianProduct.equiv {I U: Type} (X : I → Set U) : def Function.equiv {I X:Type} : (∀ _:I, X) ≃ (I → X) := { toFun f := f invFun f := f - left_inv f := rfl - right_inv f := rfl + left_inv _ := rfl + right_inv _ := rfl } def product_zero_equiv {X: Fin 0 → Type} : (∀ i:Fin 0, X i) ≃ PUnit := { @@ -147,7 +147,8 @@ theorem exists_function {X Y : Type} {P : X → Y → Prop} (h: ∀ x, ∃ y, P from `exists_function`, avoiding previous results that relied more explicitly on the axiom of choice. -/ theorem axiom_of_choice_from_exists_function {I: Type} {X: I → Type} (h : ∀ i, Nonempty (X i)) : - Nonempty (∀ i, X i) := ⟨ fun i ↦ (h i).some ⟩ + Nonempty (∀ i, X i) := by + sorry /-- Exercise 8.4.2 -/ theorem exists_set_singleton_intersect {I U:Type} {X: I → Set U} (h: Set.PairwiseDisjoint .univ X)