From 703e2804dbc90403bf750a5149e13fa2b181f5b4 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Thu, 1 Aug 2024 13:18:35 -0400 Subject: [PATCH] Golf --- SphereEversion/ToMathlib/Topology/Misc.lean | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/SphereEversion/ToMathlib/Topology/Misc.lean b/SphereEversion/ToMathlib/Topology/Misc.lean index 8d83dcf1..23aee3d9 100644 --- a/SphereEversion/ToMathlib/Topology/Misc.lean +++ b/SphereEversion/ToMathlib/Topology/Misc.lean @@ -19,10 +19,7 @@ theorem Function.LeftInverse.mem_preimage_iff (hfg : LeftInverse g f) {s : Set -- TODO: move to Data.Set.Basic theorem Function.LeftInverse.image_eq (hfg : LeftInverse g f) (s : Set α) : f '' s = range f ∩ g ⁻¹' s := by - ext x - constructor - · rintro ⟨x, hx, rfl⟩; exact ⟨mem_range_self x, hfg.mem_preimage_iff.mpr hx⟩ - · rintro ⟨⟨x, rfl⟩, b⟩; exact mem_image_of_mem f (hfg.mem_preimage_iff.mp b) + rw [inter_comm, ← image_preimage_eq_inter_range, hfg.preimage_preimage] theorem Function.LeftInverse.isOpenMap {f : α → β} {g : β → α} (hfg : LeftInverse g f) (hf : IsOpen (range f)) (hg : ContinuousOn g (range f)) : IsOpenMap f := fun U hU ↦ by