𝕜 : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_1
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
s : Set H
hs : IsOpen s
⊢ UniqueDiffOn 𝕜 (range ↑I ∩ ↑(ModelWithCorners.symm I) ⁻¹' s)
𝕜 : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_1
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
s : Set H
hs : IsOpen s
⊢ UniqueDiffOn 𝕜 (↑(ModelWithCorners.symm I) ⁻¹' s ∩ range ↑I)
rw [inter_comm]
no goals
𝕜 : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_1
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
s : Set H
hs : IsOpen s
⊢ UniqueDiffOn 𝕜 (range ↑I ∩ ↑(ModelWithCorners.symm I) ⁻¹' s)
exact I.unique_diff.inter (hs.preimage I.continuous_invFun)