α : Type u_2
β : Type u_1
γ : Type ?u.2548
δ : Type ?u.2551
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
α : Type u_2
β : Type u_1
γ : Type ?u.2548
δ : Type ?u.2551
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : T2Space β
di : DenseInducing i
hd : Dense (range iᶜ)
s : Set α
hs : IsCompact s
⊢ interior s = ∅
refine' eq_empty_iff_forall_not_mem.2 fun x hx => _
α : Type u_2
β : Type u_1
γ : Type ?u.2548
δ : Type ?u.2551
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
α : Type u_2
β : Type u_1
γ : Type ?u.2548
δ : Type ?u.2551
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
rw [mem_interior_iff_mem_nhds] at hx
α : Type u_2
β : Type u_1
γ : Type ?u.2548
δ : Type ?u.2551
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
α : Type u_2
β : Type u_1
γ : Type ?u.2548
δ : Type ?u.2551
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
have := di.closure_image_mem_nhds hx
α : Type u_2
β : Type u_1
γ : Type ?u.2548
δ : Type ?u.2551
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
α : Type u_2
β : Type u_1
γ : Type ?u.2548
δ : Type ?u.2551
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
rw [(hs.image di.continuous).isClosed.closure_eq] at this
case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.2548
δ : Type ?u.2551
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
α : Type u_2
β : Type u_1
γ : Type ?u.2548
δ : Type ?u.2551
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
rcases hd.inter_nhds_nonempty this with ⟨y, hyi, hys⟩
no goals
case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.2548
δ : Type ?u.2551
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
exact hyi (image_subset_range _ _ hys)