[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
⊢ Homeomorph.trans h (Homeomorph.symm h) = Homeomorph.refl α
[PROOFSTEP]
ext
[GOAL]
case H
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
x✝ : α
⊢ ↑(Homeomorph.trans h (Homeomorph.symm h)) x✝ = ↑(Homeomorph.refl α) x✝
[PROOFSTEP]
apply symm_apply_apply
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
⊢ Homeomorph.trans (Homeomorph.symm h) h = Homeomorph.refl β
[PROOFSTEP]
ext
[GOAL]
case H
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
x✝ : β
⊢ ↑(Homeomorph.trans (Homeomorph.symm h) h) x✝ = ↑(Homeomorph.refl β) x✝
[PROOFSTEP]
apply apply_symm_apply
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α ≃ₜ β
g : β → α
hg : Function.RightInverse g ↑f
this : g = ↑(Homeomorph.symm f)
⊢ Function.LeftInverse g ↑f
[PROOFSTEP]
convert f.left_inv
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α ≃ₜ β
g : β → α
hg : Function.RightInverse g ↑f
this : g = ↑(Homeomorph.symm f)
⊢ Function.RightInverse g ↑f
[PROOFSTEP]
convert f.right_inv using 1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α ≃ₜ β
g : β → α
hg : Function.RightInverse g ↑f
this : g = ↑(Homeomorph.symm f)
⊢ Continuous
    { toFun := ↑f, invFun := g, left_inv := (_ : Function.LeftInverse g ↑f),
        right_inv := (_ : Function.RightInverse g ↑f) }.invFun
[PROOFSTEP]
convert f.symm.continuous
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
⊢ Inducing (↑(Homeomorph.symm h) ∘ ↑h)
[PROOFSTEP]
simp only [symm_comp_self, inducing_id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
⊢ QuotientMap (↑h ∘ ↑(Homeomorph.symm h))
[PROOFSTEP]
simp only [self_comp_symm, QuotientMap.id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : Embedding f
⊢ Continuous (f ∘ (Equiv.ofInjective f (_ : Function.Injective f)).invFun)
[PROOFSTEP]
simp [continuous_subtype_val]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s : Set β
h : α ≃ₜ β
⊢ IsCompact (↑h ⁻¹' s) ↔ IsCompact s
[PROOFSTEP]
rw [← image_symm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s : Set β
h : α ≃ₜ β
⊢ IsCompact (↑(Homeomorph.symm h) '' s) ↔ IsCompact s
[PROOFSTEP]
exact h.symm.isCompact_image
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s : Set α
h : α ≃ₜ β
hs : IsPreconnected (↑h '' s)
⊢ IsPreconnected s
[PROOFSTEP]
simpa only [image_symm, preimage_image] using hs.image _ h.symm.continuous.continuousOn
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s : Set β
h : α ≃ₜ β
⊢ IsPreconnected (↑h ⁻¹' s) ↔ IsPreconnected s
[PROOFSTEP]
rw [← image_symm, isPreconnected_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s : Set β
h : α ≃ₜ β
⊢ IsConnected (↑h ⁻¹' s) ↔ IsConnected s
[PROOFSTEP]
rw [← image_symm, isConnected_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
⊢ map (↑h) (cocompact α) = cocompact β
[PROOFSTEP]
rw [← h.comap_cocompact, map_comap_of_surjective h.surjective]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
s : Set α
⊢ IsOpen (↑h '' s) ↔ IsOpen s
[PROOFSTEP]
rw [← preimage_symm, isOpen_preimage]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
s : Set β
⊢ IsClosed (↑h ⁻¹' s) ↔ IsClosed s
[PROOFSTEP]
simp only [← isOpen_compl_iff, ← preimage_compl, isOpen_preimage]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
s : Set α
⊢ IsClosed (↑h '' s) ↔ IsClosed s
[PROOFSTEP]
rw [← preimage_symm, isClosed_preimage]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
s : Set α
⊢ ↑h '' closure s = closure (↑h '' s)
[PROOFSTEP]
rw [← preimage_symm, preimage_closure]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
s : Set α
⊢ ↑h '' interior s = interior (↑h '' s)
[PROOFSTEP]
rw [← preimage_symm, preimage_interior]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
s : Set α
⊢ ↑h '' frontier s = frontier (↑h '' s)
[PROOFSTEP]
rw [← preimage_symm, preimage_frontier]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
x : α
⊢ range ↑h ∈ 𝓝 (↑h x)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
x : α
⊢ map (↑(Homeomorph.symm h)) (𝓝 (↑h x)) = 𝓝 x
[PROOFSTEP]
rw [h.symm.map_nhds_eq, h.symm_apply_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
y : β
⊢ comap (↑h) (𝓝 y) = 𝓝 (↑(Homeomorph.symm h) y)
[PROOFSTEP]
rw [h.nhds_eq_comap, h.apply_symm_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
i : LocallyConnectedSpace β
h : α ≃ₜ β
⊢ LocallyConnectedSpace α
[PROOFSTEP]
have : ∀ x, (𝓝 x).HasBasis (fun s ↦ IsOpen s ∧ h x ∈ s ∧ IsConnected s) (h.symm '' ·) := fun x ↦
  by
  rw [← h.symm_map_nhds_eq]
  exact (i.1 _).map _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
i : LocallyConnectedSpace β
h : α ≃ₜ β
x : α
⊢ HasBasis (𝓝 x) (fun s => IsOpen s ∧ ↑h x ∈ s ∧ IsConnected s) fun x => ↑(Homeomorph.symm h) '' x
[PROOFSTEP]
rw [← h.symm_map_nhds_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
i : LocallyConnectedSpace β
h : α ≃ₜ β
x : α
⊢ HasBasis (map (↑(Homeomorph.symm h)) (𝓝 (↑h x))) (fun s => IsOpen s ∧ ↑h x ∈ s ∧ IsConnected s) fun x =>
    ↑(Homeomorph.symm h) '' x
[PROOFSTEP]
exact (i.1 _).map _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
i : LocallyConnectedSpace β
h : α ≃ₜ β
this : ∀ (x : α), HasBasis (𝓝 x) (fun s => IsOpen s ∧ ↑h x ∈ s ∧ IsConnected s) fun x => ↑(Homeomorph.symm h) '' x
⊢ LocallyConnectedSpace α
[PROOFSTEP]
refine locallyConnectedSpace_of_connected_bases _ _ this fun _ _ hs ↦ ?_
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
i : LocallyConnectedSpace β
h : α ≃ₜ β
this : ∀ (x : α), HasBasis (𝓝 x) (fun s => IsOpen s ∧ ↑h x ∈ s ∧ IsConnected s) fun x => ↑(Homeomorph.symm h) '' x
x✝¹ : α
x✝ : Set β
hs : IsOpen x✝ ∧ ↑h x✝¹ ∈ x✝ ∧ IsConnected x✝
⊢ IsPreconnected (↑(Homeomorph.symm h) '' x✝)
[PROOFSTEP]
exact hs.2.2.2.image _ h.symm.continuous.continuousOn
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : α ≃ β
h₁ : Continuous ↑e
h₂ : IsOpenMap ↑e
⊢ Continuous e.invFun
[PROOFSTEP]
rw [continuous_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : α ≃ β
h₁ : Continuous ↑e
h₂ : IsOpenMap ↑e
⊢ ∀ (s : Set α), IsOpen s → IsOpen (e.invFun ⁻¹' s)
[PROOFSTEP]
intro s hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : α ≃ β
h₁ : Continuous ↑e
h₂ : IsOpenMap ↑e
s : Set α
hs : IsOpen s
⊢ IsOpen (e.invFun ⁻¹' s)
[PROOFSTEP]
convert ← h₂ s hs using 1
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : α ≃ β
h₁ : Continuous ↑e
h₂ : IsOpenMap ↑e
s : Set α
hs : IsOpen s
⊢ ↑e '' s = e.invFun ⁻¹' s
[PROOFSTEP]
apply e.image_eq_preimage
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
f : β → γ
x : α
⊢ range ↑h ∈ 𝓝 (↑h x)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
f : γ → α
⊢ IsOpenMap (↑h ∘ f) ↔ IsOpenMap f
[PROOFSTEP]
refine' ⟨_, fun hf => h.isOpenMap.comp hf⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
f : γ → α
⊢ IsOpenMap (↑h ∘ f) → IsOpenMap f
[PROOFSTEP]
intro hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
f : γ → α
hf : IsOpenMap (↑h ∘ f)
⊢ IsOpenMap f
[PROOFSTEP]
rw [← Function.comp.left_id f, ← h.symm_comp_self, Function.comp.assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
f : γ → α
hf : IsOpenMap (↑h ∘ f)
⊢ IsOpenMap (↑(Homeomorph.symm h) ∘ ↑h ∘ f)
[PROOFSTEP]
exact h.symm.isOpenMap.comp hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
f : β → γ
⊢ IsOpenMap (f ∘ ↑h) ↔ IsOpenMap f
[PROOFSTEP]
refine' ⟨_, fun hf => hf.comp h.isOpenMap⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
f : β → γ
⊢ IsOpenMap (f ∘ ↑h) → IsOpenMap f
[PROOFSTEP]
intro hf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
f : β → γ
hf : IsOpenMap (f ∘ ↑h)
⊢ IsOpenMap f
[PROOFSTEP]
rw [← Function.comp.right_id f, ← h.self_comp_symm, ← Function.comp.assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
f : β → γ
hf : IsOpenMap (f ∘ ↑h)
⊢ IsOpenMap ((f ∘ ↑h) ∘ ↑(Homeomorph.symm h))
[PROOFSTEP]
exact hf.comp h.symm.isOpenMap
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
ι : Type u_5
p : ι → Prop
β : ι → Type u_6
inst✝¹ : (i : ι) → TopologicalSpace (β i)
inst✝ : DecidablePred p
⊢ Continuous (Equiv.piEquivPiSubtypeProd p β).toFun
[PROOFSTEP]
apply Continuous.prod_mk
[GOAL]
case hf
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
ι : Type u_5
p : ι → Prop
β : ι → Type u_6
inst✝¹ : (i : ι) → TopologicalSpace (β i)
inst✝ : DecidablePred p
⊢ Continuous fun x x_1 => x ↑x_1
[PROOFSTEP]
exact continuous_pi fun j => continuous_apply j.1
[GOAL]
case hg
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
ι : Type u_5
p : ι → Prop
β : ι → Type u_6
inst✝¹ : (i : ι) → TopologicalSpace (β i)
inst✝ : DecidablePred p
⊢ Continuous fun x x_1 => x ↑x_1
[PROOFSTEP]
exact continuous_pi fun j => continuous_apply j.1
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
ι : Type u_5
p : ι → Prop
β : ι → Type u_6
inst✝¹ : (i : ι) → TopologicalSpace (β i)
inst✝ : DecidablePred p
j : ι
⊢ Continuous fun a => Equiv.invFun (Equiv.piEquivPiSubtypeProd p β) a j
[PROOFSTEP]
dsimp only [Equiv.piEquivPiSubtypeProd]
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
ι : Type u_5
p : ι → Prop
β : ι → Type u_6
inst✝¹ : (i : ι) → TopologicalSpace (β i)
inst✝ : DecidablePred p
j : ι
⊢ Continuous fun a => if h : p j then Prod.fst a { val := j, property := h } else Prod.snd a { val := j, property := h }
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
ι : Type u_5
p : ι → Prop
β : ι → Type u_6
inst✝¹ : (i : ι) → TopologicalSpace (β i)
inst✝ : DecidablePred p
j : ι
h✝ : p j
⊢ Continuous fun a => Prod.fst a { val := j, property := h✝ }
case neg
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
ι : Type u_5
p : ι → Prop
β : ι → Type u_6
inst✝¹ : (i : ι) → TopologicalSpace (β i)
inst✝ : DecidablePred p
j : ι
h✝ : ¬p j
⊢ Continuous fun a => Prod.snd a { val := j, property := h✝ }
[PROOFSTEP]
exacts [(continuous_apply _).comp continuous_fst, (continuous_apply _).comp continuous_snd]
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
ι : Type u_5
inst✝¹ : DecidableEq ι
i : ι
β : ι → Type u_6
inst✝ : (j : ι) → TopologicalSpace (β j)
j : ι
⊢ Continuous fun a => Equiv.invFun (Equiv.piSplitAt i β) a j
[PROOFSTEP]
dsimp only [Equiv.piSplitAt]
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
ι : Type u_5
inst✝¹ : DecidableEq ι
i : ι
β : ι → Type u_6
inst✝ : (j : ι) → TopologicalSpace (β j)
j : ι
⊢ Continuous fun a => if h : j = i then (_ : i = j) ▸ a.fst else Prod.snd a { val := j, property := h }
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
ι : Type u_5
inst✝¹ : DecidableEq ι
i : ι
β : ι → Type u_6
inst✝ : (j : ι) → TopologicalSpace (β j)
j : ι
h : j = i
⊢ Continuous fun a => (_ : i = j) ▸ a.fst
case neg
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
ι : Type u_5
inst✝¹ : DecidableEq ι
i : ι
β : ι → Type u_6
inst✝ : (j : ι) → TopologicalSpace (β j)
j : ι
h : ¬j = i
⊢ Continuous fun a => Prod.snd a { val := j, property := h }
[PROOFSTEP]
subst h
[GOAL]
case pos
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
ι : Type u_5
inst✝¹ : DecidableEq ι
β : ι → Type u_6
inst✝ : (j : ι) → TopologicalSpace (β j)
j : ι
⊢ Continuous fun a => (_ : j = j) ▸ a.fst
case neg
α : Type u_1
β✝ : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β✝
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
ι : Type u_5
inst✝¹ : DecidableEq ι
i : ι
β : ι → Type u_6
inst✝ : (j : ι) → TopologicalSpace (β j)
j : ι
h : ¬j = i
⊢ Continuous fun a => Prod.snd a { val := j, property := h }
[PROOFSTEP]
exacts [continuous_fst, (continuous_apply _).comp continuous_snd]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α ≃ β
hf : Inducing ↑f
⊢ Continuous
    (↑f ∘
      { toFun := f.toFun, invFun := f.invFun, left_inv := (_ : Function.LeftInverse f.invFun f.toFun),
          right_inv := (_ : Function.RightInverse f.invFun f.toFun) }.invFun)
[PROOFSTEP]
simpa using continuous_id
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CompactSpace α
inst✝ : T2Space β
f : α ≃ β
hf : Continuous ↑f
⊢ Continuous ↑f.symm
[PROOFSTEP]
rw [continuous_iff_isClosed]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CompactSpace α
inst✝ : T2Space β
f : α ≃ β
hf : Continuous ↑f
⊢ ∀ (s : Set α), IsClosed s → IsClosed (↑f.symm ⁻¹' s)
[PROOFSTEP]
intro C hC
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CompactSpace α
inst✝ : T2Space β
f : α ≃ β
hf : Continuous ↑f
C : Set α
hC : IsClosed C
⊢ IsClosed (↑f.symm ⁻¹' C)
[PROOFSTEP]
have hC' : IsClosed (f '' C) := (hC.isCompact.image hf).isClosed
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CompactSpace α
inst✝ : T2Space β
f : α ≃ β
hf : Continuous ↑f
C : Set α
hC : IsClosed C
hC' : IsClosed (↑f '' C)
⊢ IsClosed (↑f.symm ⁻¹' C)
[PROOFSTEP]
rwa [Equiv.image_eq_preimage] at hC' 
