case h₁
α : Type u_1
β : Type u_2
γ : Type ?u.108605
δ : Type ?u.108608
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ Continuous ↑e

case h₂
α : Type u_1
β : Type u_2
γ : Type ?u.108605
δ : Type ?u.108608
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ Injective ↑e

case h₃
α : Type u_1
β : Type u_2
γ : Type ?u.108605
δ : Type ?u.108608
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ IsOpenMap ↑e
α : Type u_1
β : Type u_2
γ : Type ?u.108605
δ : Type ?u.108608
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ OpenEmbedding ↑e
apply openEmbedding_of_continuous_injective_open
case h₁
α : Type u_1
β : Type u_2
γ : Type ?u.108605
δ : Type ?u.108608
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ ContinuousOn (↑e) univ
case h₁
α : Type u_1
β : Type u_2
γ : Type ?u.108605
δ : Type ?u.108608
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ Continuous ↑e
apply continuous_iff_continuousOn_univ.mpr
case h₁
α : Type u_1
β : Type u_2
γ : Type ?u.108605
δ : Type ?u.108608
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ ContinuousOn (↑e) e.source
case h₁
α : Type u_1
β : Type u_2
γ : Type ?u.108605
δ : Type ?u.108608
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ ContinuousOn (↑e) univ
rw [← h]
no goals
case h₁
α : Type u_1
β : Type u_2
γ : Type ?u.108605
δ : Type ?u.108608
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ ContinuousOn (↑e) e.source
exact e.continuousOn
case h₂
α : Type u_1
β : Type u_2
γ : Type ?u.108605
δ : Type ?u.108608
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ InjOn (↑e) univ
case h₂
α : Type u_1
β : Type u_2
γ : Type ?u.108605
δ : Type ?u.108608
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ Injective ↑e
apply Set.injective_iff_injOn_univ.mpr
case h₂
α : Type u_1
β : Type u_2
γ : Type ?u.108605
δ : Type ?u.108608
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ InjOn (↑e) e.source
case h₂
α : Type u_1
β : Type u_2
γ : Type ?u.108605
δ : Type ?u.108608
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ InjOn (↑e) univ
rw [← h]
no goals
case h₂
α : Type u_1
β : Type u_2
γ : Type ?u.108605
δ : Type ?u.108608
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ InjOn (↑e) e.source
exact e.injOn
case h₃
α : Type u_1
β : Type u_2
γ : Type ?u.108605
δ : Type ?u.108608
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
U : Set α
hU : IsOpen U
⊢ IsOpen (↑e '' U)
case h₃
α : Type u_1
β : Type u_2
γ : Type ?u.108605
δ : Type ?u.108608
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
⊢ IsOpenMap ↑e
intro U hU
no goals
case h₃
α : Type u_1
β : Type u_2
γ : Type ?u.108605
δ : Type ?u.108608
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
h : e.source = univ
U : Set α
hU : IsOpen U
⊢ IsOpen (↑e '' U)
simpa only [h, subset_univ, mfld_simps] using e.image_open_of_open hU