From 19ab970d5f9f0204e7bb92cb15cf9862bf3ef449 Mon Sep 17 00:00:00 2001 From: grunweg Date: Fri, 26 Jan 2024 08:27:37 +0000 Subject: [PATCH] feat: add PartialHomeomorph.extend_target' (#9977) Inspired by sphere-eversion; similar to `PartialEquiv.image_source_eq_target`. --- Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean b/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean index b5a692212bd60..e6403df8ef98c 100644 --- a/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean +++ b/Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean @@ -980,6 +980,9 @@ theorem extend_target : (f.extend I).target = I.symm ⁻¹' f.target ∩ range I simp_rw [extend, PartialEquiv.trans_target, I.target_eq, I.toPartialEquiv_coe_symm, inter_comm] #align local_homeomorph.extend_target PartialHomeomorph.extend_target +theorem extend_target' : (f.extend I).target = I '' f.target := by + rw [extend, PartialEquiv.trans_target'', I.source_eq, univ_inter, I.toPartialEquiv_coe] + lemma isOpen_extend_target [I.Boundaryless] : IsOpen (f.extend I).target := by rw [extend_target, I.range_eq_univ, inter_univ] exact I.continuous_symm.isOpen_preimage _ f.open_target