From 2d8e0df12122f88f6a510972499e988616b220b2 Mon Sep 17 00:00:00 2001 From: Marcus Zibrowius Date: Tue, 3 Sep 2024 17:05:49 +0200 Subject: [PATCH] more ideas on Boss of FunctionBij --- development-status.md | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/development-status.md b/development-status.md index 754045b..a5fa2d5 100644 --- a/development-status.md +++ b/development-status.md @@ -266,7 +266,6 @@ Hopefully, `Fin n` will be explained elsewhere. My own solution was rather long: ```` example {A B : Type} {f : A → B} : Injective (preimage f) ↔ Surjective f := by - rw [surjective_iff_nonempty_fibres] constructor · intro h_inj intro b @@ -321,7 +320,21 @@ It might be useful to have one part of the Boss level of FunctionInj available h lemma surjective_iff_nonempty_fibres {A B : Type} (f : A → B) : Surjective f ↔ ∀ b : B, ∃ (a : A), a ∈ (f ⁻¹' { b }) := by sorry ```` + But I haven't managed to find a more satisfactory solution by assuming this lemma. -======= the two sides of the equivalence are almost identical! Perhaps modify question so that they *are* identical? +The second part can be solved more elegantly using +```` +Function.Surjective.image_preimage.{u_1, u_2} {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Surjective f) + (s : Set β) : f '' (f ⁻¹' s) = s +```` +Using this theorem, which could be a separate exercise in FunctionSurj, the second half above becomes: +```` +· intro h_surj + intro s s' hs + apply congr_arg (image f) at hs + rw [h_surj.image_preimage] at hs + rw [h_surj.image_preimage] at hs + assumption +````