[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
s : Set α
a : α
di : DenseInducing i
hs : s ∈ 𝓝 a
⊢ closure (i '' s) ∈ 𝓝 (i a)
[PROOFSTEP]
rw [di.nhds_eq_comap a, ((nhds_basis_opens _).comap _).mem_iff] at hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
s : Set α
a : α
di : DenseInducing i
hs : ∃ i_1, (i a ∈ i_1 ∧ IsOpen i_1) ∧ i ⁻¹' i_1 ⊆ s
⊢ closure (i '' s) ∈ 𝓝 (i a)
[PROOFSTEP]
rcases hs with ⟨U, ⟨haU, hUo⟩, sub : i ⁻¹' U ⊆ s⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
s : Set α
a : α
di : DenseInducing i
U : Set β
sub : i ⁻¹' U ⊆ s
haU : i a ∈ U
hUo : IsOpen U
⊢ closure (i '' s) ∈ 𝓝 (i a)
[PROOFSTEP]
refine' mem_of_superset (hUo.mem_nhds haU) _
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
s : Set α
a : α
di : DenseInducing i
U : Set β
sub : i ⁻¹' U ⊆ s
haU : i a ∈ U
hUo : IsOpen U
⊢ U ⊆ closure (i '' s)
[PROOFSTEP]
calc
  U ⊆ closure (i '' (i ⁻¹' U)) := di.dense.subset_closure_image_preimage_of_isOpen hUo
  _ ⊆ closure (i '' s) := closure_mono (image_subset i sub)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di✝ di : DenseInducing i
s : Set α
⊢ Dense (i '' s) ↔ Dense s
[PROOFSTEP]
refine' ⟨fun H x => _, di.dense.dense_image di.continuous⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di✝ di : DenseInducing i
s : Set α
H : Dense (i '' s)
x : α
⊢ x ∈ closure s
[PROOFSTEP]
rw [di.toInducing.closure_eq_preimage_closure_image, H.closure_eq, preimage_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di✝ di : DenseInducing i
s : Set α
H : Dense (i '' s)
x : α
⊢ x ∈ univ
[PROOFSTEP]
trivial
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : T2Space β
di : DenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
⊢ interior s = ∅
[PROOFSTEP]
refine' eq_empty_iff_forall_not_mem.2 fun x hx => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : T2Space β
di : DenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
x : α
hx : x ∈ interior s
⊢ False
[PROOFSTEP]
rw [mem_interior_iff_mem_nhds] at hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : T2Space β
di : DenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
x : α
hx : s ∈ 𝓝 x
⊢ False
[PROOFSTEP]
have := di.closure_image_mem_nhds hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : T2Space β
di : DenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
x : α
hx : s ∈ 𝓝 x
this : closure (i '' s) ∈ 𝓝 (i x)
⊢ False
[PROOFSTEP]
rw [(hs.image di.continuous).isClosed.closure_eq] at this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : T2Space β
di : DenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
x : α
hx : s ∈ 𝓝 x
this : i '' s ∈ 𝓝 (i x)
⊢ False
[PROOFSTEP]
rcases hd.inter_nhds_nonempty this with ⟨y, hyi, hys⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : T2Space β
di : DenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
x : α
hx : s ∈ 𝓝 x
this : i '' s ∈ 𝓝 (i x)
y : β
hyi : y ∈ (range i)ᶜ
hys : y ∈ i '' s
⊢ False
[PROOFSTEP]
exact hyi (image_subset_range _ _ hys)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : DenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
⊢ Tendsto f (comap g (𝓝 d)) (𝓝 a)
[PROOFSTEP]
have lim1 : map g (comap g (𝓝 d)) ≤ 𝓝 d := map_comap_le
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : DenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map g (comap g (𝓝 d)) ≤ 𝓝 d
⊢ Tendsto f (comap g (𝓝 d)) (𝓝 a)
[PROOFSTEP]
replace lim1 : map h (map g (comap g (𝓝 d))) ≤ map h (𝓝 d) := map_mono lim1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : DenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map h (map g (comap g (𝓝 d))) ≤ map h (𝓝 d)
⊢ Tendsto f (comap g (𝓝 d)) (𝓝 a)
[PROOFSTEP]
rw [Filter.map_map, comm, ← Filter.map_map, map_le_iff_le_comap] at lim1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : DenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map f (comap g (𝓝 d)) ≤ comap i (map h (𝓝 d))
⊢ Tendsto f (comap g (𝓝 d)) (𝓝 a)
[PROOFSTEP]
have lim2 : comap i (map h (𝓝 d)) ≤ comap i (𝓝 (i a)) := comap_mono H
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : DenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map f (comap g (𝓝 d)) ≤ comap i (map h (𝓝 d))
lim2 : comap i (map h (𝓝 d)) ≤ comap i (𝓝 (i a))
⊢ Tendsto f (comap g (𝓝 d)) (𝓝 a)
[PROOFSTEP]
rw [← di.nhds_eq_comap] at lim2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : DenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map f (comap g (𝓝 d)) ≤ comap i (map h (𝓝 d))
lim2 : comap i (map h (𝓝 d)) ≤ 𝓝 a
⊢ Tendsto f (comap g (𝓝 d)) (𝓝 a)
[PROOFSTEP]
exact le_trans lim1 lim2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
di : DenseInducing i
b : β
s : Set β
hs : s ∈ 𝓝 b
⊢ ∃ a, i a ∈ s
[PROOFSTEP]
rcases mem_closure_iff_nhds.1 (di.dense b) s hs with ⟨_, ⟨ha, a, rfl⟩⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
di : DenseInducing i
b : β
s : Set β
hs : s ∈ 𝓝 b
a : α
ha : i a ∈ s
⊢ ∃ a, i a ∈ s
[PROOFSTEP]
exact ⟨a, ha⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
f : α → γ
di : DenseInducing i
hf : ∀ (b : β), ∃ c, Tendsto f (comap i (𝓝 b)) (𝓝 c)
a : α
⊢ extend di f (i a) = f a
[PROOFSTEP]
rcases hf (i a) with ⟨b, hb⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
f : α → γ
di : DenseInducing i
hf : ∀ (b : β), ∃ c, Tendsto f (comap i (𝓝 b)) (𝓝 c)
a : α
b : γ
hb : Tendsto f (comap i (𝓝 (i a))) (𝓝 b)
⊢ extend di f (i a) = f a
[PROOFSTEP]
refine' di.extend_eq_at' b _
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
f : α → γ
di : DenseInducing i
hf : ∀ (b : β), ∃ c, Tendsto f (comap i (𝓝 b)) (𝓝 c)
a : α
b : γ
hb : Tendsto f (comap i (𝓝 (i a))) (𝓝 b)
⊢ Tendsto f (𝓝 a) (𝓝 b)
[PROOFSTEP]
rwa [← di.toInducing.nhds_eq_comap] at hb
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g✝ : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
b : β
f : α → γ
g : β → γ
di : DenseInducing i
hf : ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) = f x
hg : ContinuousAt g b
⊢ extend di f b = g b
[PROOFSTEP]
refine' di.extend_eq_of_tendsto fun s hs => mem_map.2 _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g✝ : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
b : β
f : α → γ
g : β → γ
di : DenseInducing i
hf : ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) = f x
hg : ContinuousAt g b
s : Set γ
hs : s ∈ 𝓝 (g b)
⊢ f ⁻¹' s ∈ comap i (𝓝 b)
[PROOFSTEP]
suffices : ∀ᶠ x : α in comap i (𝓝 b), g (i x) ∈ s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g✝ : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
b : β
f : α → γ
g : β → γ
di : DenseInducing i
hf : ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) = f x
hg : ContinuousAt g b
s : Set γ
hs : s ∈ 𝓝 (g b)
this : ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) ∈ s
⊢ f ⁻¹' s ∈ comap i (𝓝 b)
case this
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g✝ : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
b : β
f : α → γ
g : β → γ
di : DenseInducing i
hf : ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) = f x
hg : ContinuousAt g b
s : Set γ
hs : s ∈ 𝓝 (g b)
⊢ ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) ∈ s
[PROOFSTEP]
exact hf.mp (this.mono fun x hgx hfx => hfx ▸ hgx)
[GOAL]
case this
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g✝ : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
b : β
f : α → γ
g : β → γ
di : DenseInducing i
hf : ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) = f x
hg : ContinuousAt g b
s : Set γ
hs : s ∈ 𝓝 (g b)
⊢ ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) ∈ s
[PROOFSTEP]
clear hf f
[GOAL]
case this
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f : γ → α
g✝ : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
b : β
g : β → γ
di : DenseInducing i
hg : ContinuousAt g b
s : Set γ
hs : s ∈ 𝓝 (g b)
⊢ ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) ∈ s
[PROOFSTEP]
refine' eventually_comap.2 ((hg.eventually hs).mono _)
[GOAL]
case this
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f : γ → α
g✝ : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
b : β
g : β → γ
di : DenseInducing i
hg : ContinuousAt g b
s : Set γ
hs : s ∈ 𝓝 (g b)
⊢ ∀ (x : β), s (g x) → ∀ (a : α), i a = x → g (i a) ∈ s
[PROOFSTEP]
rintro _ hxs x rfl
[GOAL]
case this
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f : γ → α
g✝ : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
b : β
g : β → γ
di : DenseInducing i
hg : ContinuousAt g b
s : Set γ
hs : s ∈ 𝓝 (g b)
x : α
hxs : s (g (i x))
⊢ g (i x) ∈ s
[PROOFSTEP]
exact hxs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
⊢ ContinuousAt (extend di f) b
[PROOFSTEP]
set φ := di.extend f
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
⊢ ContinuousAt φ b
[PROOFSTEP]
haveI := di.comap_nhds_neBot
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
⊢ ContinuousAt φ b
[PROOFSTEP]
suffices ∀ V' ∈ 𝓝 (φ b), IsClosed V' → φ ⁻¹' V' ∈ 𝓝 b by
  simpa [ContinuousAt, (closed_nhds_basis (φ b)).tendsto_right_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this✝ : ∀ (b : β), NeBot (comap i (𝓝 b))
this : ∀ (V' : Set γ), V' ∈ 𝓝 (φ b) → IsClosed V' → φ ⁻¹' V' ∈ 𝓝 b
⊢ ContinuousAt φ b
[PROOFSTEP]
simpa [ContinuousAt, (closed_nhds_basis (φ b)).tendsto_right_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
⊢ ∀ (V' : Set γ), V' ∈ 𝓝 (φ b) → IsClosed V' → φ ⁻¹' V' ∈ 𝓝 b
[PROOFSTEP]
intro V' V'_in V'_closed
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed V'
⊢ φ ⁻¹' V' ∈ 𝓝 b
[PROOFSTEP]
set V₁ := {x | Tendsto f (comap i <| 𝓝 x) (𝓝 <| φ x)}
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
⊢ φ ⁻¹' V' ∈ 𝓝 b
[PROOFSTEP]
have V₁_in : V₁ ∈ 𝓝 b := by
  filter_upwards [hf]
  rintro x ⟨c, hc⟩
  rwa [di.extend_eq_of_tendsto hc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
⊢ V₁ ∈ 𝓝 b
[PROOFSTEP]
filter_upwards [hf]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
⊢ ∀ (a : β), (∃ c, Tendsto f (comap i (𝓝 a)) (𝓝 c)) → Tendsto f (comap i (𝓝 a)) (𝓝 (extend di f a))
[PROOFSTEP]
rintro x ⟨c, hc⟩
[GOAL]
case h.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
x : β
c : γ
hc : Tendsto f (comap i (𝓝 x)) (𝓝 c)
⊢ Tendsto f (comap i (𝓝 x)) (𝓝 (extend di f x))
[PROOFSTEP]
rwa [di.extend_eq_of_tendsto hc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
⊢ φ ⁻¹' V' ∈ 𝓝 b
[PROOFSTEP]
obtain ⟨V₂, V₂_in, V₂_op, hV₂⟩ : ∃ V₂ ∈ 𝓝 b, IsOpen V₂ ∧ ∀ x ∈ i ⁻¹' V₂, f x ∈ V' := by
  simpa [and_assoc] using ((nhds_basis_opens' b).comap i).tendsto_left_iff.mp (mem_of_mem_nhds V₁_in : b ∈ V₁) V' V'_in
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
⊢ ∃ V₂, V₂ ∈ 𝓝 b ∧ IsOpen V₂ ∧ ∀ (x : α), x ∈ i ⁻¹' V₂ → f x ∈ V'
[PROOFSTEP]
simpa [and_assoc] using ((nhds_basis_opens' b).comap i).tendsto_left_iff.mp (mem_of_mem_nhds V₁_in : b ∈ V₁) V' V'_in
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
V₂ : Set β
V₂_in : V₂ ∈ 𝓝 b
V₂_op : IsOpen V₂
hV₂ : ∀ (x : α), x ∈ i ⁻¹' V₂ → f x ∈ V'
⊢ φ ⁻¹' V' ∈ 𝓝 b
[PROOFSTEP]
suffices ∀ x ∈ V₁ ∩ V₂, φ x ∈ V' by filter_upwards [inter_mem V₁_in V₂_in] using this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this✝ : ∀ (b : β), NeBot (comap i (𝓝 b))
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
V₂ : Set β
V₂_in : V₂ ∈ 𝓝 b
V₂_op : IsOpen V₂
hV₂ : ∀ (x : α), x ∈ i ⁻¹' V₂ → f x ∈ V'
this : ∀ (x : β), x ∈ V₁ ∩ V₂ → φ x ∈ V'
⊢ φ ⁻¹' V' ∈ 𝓝 b
[PROOFSTEP]
filter_upwards [inter_mem V₁_in V₂_in] using this
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
V₂ : Set β
V₂_in : V₂ ∈ 𝓝 b
V₂_op : IsOpen V₂
hV₂ : ∀ (x : α), x ∈ i ⁻¹' V₂ → f x ∈ V'
⊢ ∀ (x : β), x ∈ V₁ ∩ V₂ → φ x ∈ V'
[PROOFSTEP]
rintro x ⟨x_in₁, x_in₂⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
V₂ : Set β
V₂_in : V₂ ∈ 𝓝 b
V₂_op : IsOpen V₂
hV₂ : ∀ (x : α), x ∈ i ⁻¹' V₂ → f x ∈ V'
x : β
x_in₁ : x ∈ V₁
x_in₂ : x ∈ V₂
⊢ φ x ∈ V'
[PROOFSTEP]
have hV₂x : V₂ ∈ 𝓝 x := IsOpen.mem_nhds V₂_op x_in₂
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
V₂ : Set β
V₂_in : V₂ ∈ 𝓝 b
V₂_op : IsOpen V₂
hV₂ : ∀ (x : α), x ∈ i ⁻¹' V₂ → f x ∈ V'
x : β
x_in₁ : x ∈ V₁
x_in₂ : x ∈ V₂
hV₂x : V₂ ∈ 𝓝 x
⊢ φ x ∈ V'
[PROOFSTEP]
apply V'_closed.mem_of_tendsto x_in₁
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
V₂ : Set β
V₂_in : V₂ ∈ 𝓝 b
V₂_op : IsOpen V₂
hV₂ : ∀ (x : α), x ∈ i ⁻¹' V₂ → f x ∈ V'
x : β
x_in₁ : x ∈ V₁
x_in₂ : x ∈ V₂
hV₂x : V₂ ∈ 𝓝 x
⊢ ∀ᶠ (x : α) in comap i (𝓝 x), f x ∈ V'
[PROOFSTEP]
use V₂
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
V₂ : Set β
V₂_in : V₂ ∈ 𝓝 b
V₂_op : IsOpen V₂
hV₂ : ∀ (x : α), x ∈ i ⁻¹' V₂ → f x ∈ V'
x : β
x_in₁ : x ∈ V₁
x_in₂ : x ∈ V₂
hV₂x : V₂ ∈ 𝓝 x
⊢ V₂ ∈ 𝓝 x ∧ i ⁻¹' V₂ ⊆ {x | (fun x => f x ∈ V') x}
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i✝ : α → β
di : DenseInducing i✝
inst✝¹ : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
inst✝ : TopologicalSpace γ
i : α → β
c : Continuous i
dense : ∀ (x : β), x ∈ closure (range i)
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 (i a) ∧ ∀ (b : α), i b ∈ t → b ∈ s
a : α
⊢ comap i (𝓝 (i a)) ≤ 𝓝 a
[PROOFSTEP]
simpa [Filter.le_def] using H a
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : α → β
de : DenseEmbedding e
p : α → Prop
x✝ : { x // p x }
x : α
hx : p x
⊢ 𝓝 { val := x, property := hx } = comap (subtypeEmb p e) (𝓝 (subtypeEmb p e { val := x, property := hx }))
[PROOFSTEP]
simp [subtypeEmb, nhds_subtype_eq_comap, de.toInducing.nhds_eq_comap, comap_comap, (· ∘ ·)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : α → β
de : DenseEmbedding e
p : α → Prop
⊢ closure (range (subtypeEmb p e)) = univ
[PROOFSTEP]
ext ⟨x, hx⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : α → β
de : DenseEmbedding e
p : α → Prop
x : β
hx : x ∈ closure (e '' {x | p x})
⊢ { val := x, property := hx } ∈ closure (range (subtypeEmb p e)) ↔ { val := x, property := hx } ∈ univ
[PROOFSTEP]
rw [image_eq_range] at hx
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : α → β
de : DenseEmbedding e
p : α → Prop
x : β
hx✝ : x ∈ closure (e '' {x | p x})
hx : x ∈ closure (range fun x => e ↑x)
⊢ { val := x, property := hx✝ } ∈ closure (range (subtypeEmb p e)) ↔ { val := x, property := hx✝ } ∈ univ
[PROOFSTEP]
simpa [closure_subtype, ← range_comp, (· ∘ ·)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : HasBasis (𝓝 x) p s
f : α → β
hf : DenseInducing f
⊢ HasBasis (𝓝 (f x)) p fun i => closure (f '' s i)
[PROOFSTEP]
rw [Filter.hasBasis_iff] at h ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
⊢ ∀ (t : Set β), t ∈ 𝓝 (f x) ↔ ∃ i, p i ∧ closure (f '' s i) ⊆ t
[PROOFSTEP]
intro T
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
⊢ T ∈ 𝓝 (f x) ↔ ∃ i, p i ∧ closure (f '' s i) ⊆ T
[PROOFSTEP]
refine' ⟨fun hT => _, fun hT => _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
⊢ ∃ i, p i ∧ closure (f '' s i) ⊆ T
[PROOFSTEP]
obtain ⟨T', hT₁, hT₂, hT₃⟩ := exists_mem_nhds_isClosed_subset hT
[GOAL]
case refine'_1.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed T'
hT₃ : T' ⊆ T
⊢ ∃ i, p i ∧ closure (f '' s i) ⊆ T
[PROOFSTEP]
have hT₄ : f ⁻¹' T' ∈ 𝓝 x := by
  rw [hf.toInducing.nhds_eq_comap x]
  exact ⟨T', hT₁, Subset.rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed T'
hT₃ : T' ⊆ T
⊢ f ⁻¹' T' ∈ 𝓝 x
[PROOFSTEP]
rw [hf.toInducing.nhds_eq_comap x]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed T'
hT₃ : T' ⊆ T
⊢ f ⁻¹' T' ∈ Filter.comap f (𝓝 (f x))
[PROOFSTEP]
exact ⟨T', hT₁, Subset.rfl⟩
[GOAL]
case refine'_1.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed T'
hT₃ : T' ⊆ T
hT₄ : f ⁻¹' T' ∈ 𝓝 x
⊢ ∃ i, p i ∧ closure (f '' s i) ⊆ T
[PROOFSTEP]
obtain ⟨i, hi, hi'⟩ := (h _).mp hT₄
[GOAL]
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed T'
hT₃ : T' ⊆ T
hT₄ : f ⁻¹' T' ∈ 𝓝 x
i : ι
hi : p i
hi' : s i ⊆ f ⁻¹' T'
⊢ ∃ i, p i ∧ closure (f '' s i) ⊆ T
[PROOFSTEP]
exact
  ⟨i, hi,
    (closure_mono (image_subset f hi')).trans (Subset.trans (closure_minimal (image_preimage_subset _ _) hT₂) hT₃)⟩
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
hT : ∃ i, p i ∧ closure (f '' s i) ⊆ T
⊢ T ∈ 𝓝 (f x)
[PROOFSTEP]
obtain ⟨i, hi, hi'⟩ := hT
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
i : ι
hi : p i
hi' : closure (f '' s i) ⊆ T
⊢ T ∈ 𝓝 (f x)
[PROOFSTEP]
suffices closure (f '' s i) ∈ 𝓝 (f x) by filter_upwards [this] using hi'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
i : ι
hi : p i
hi' : closure (f '' s i) ⊆ T
this : closure (f '' s i) ∈ 𝓝 (f x)
⊢ T ∈ 𝓝 (f x)
[PROOFSTEP]
filter_upwards [this] using hi'
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
i : ι
hi : p i
hi' : closure (f '' s i) ⊆ T
⊢ closure (f '' s i) ∈ 𝓝 (f x)
[PROOFSTEP]
replace h := (h (s i)).mpr ⟨i, hi, Subset.rfl⟩
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
f : α → β
hf : DenseInducing f
T : Set β
i : ι
hi : p i
hi' : closure (f '' s i) ⊆ T
h : s i ∈ 𝓝 x
⊢ closure (f '' s i) ∈ 𝓝 (f x)
[PROOFSTEP]
exact hf.closure_image_mem_nhds h


[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'