α : Type u_1
β : Type u_2
γ : Type ?u.1224
δ : Type ?u.1227
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)
α : Type u_1
β : Type u_2
γ : Type ?u.1224
δ : Type ?u.1227
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
s : Set α
a : α
di : DenseInducing i
hs : s ∈ 𝓝 a
⊢ closure (i '' s) ∈ 𝓝 (i a)
rw [di.nhds_eq_comap a, ((nhds_basis_opens _).comap _).mem_iff] at hs
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.1224
δ : Type ?u.1227
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)
α : Type u_1
β : Type u_2
γ : Type ?u.1224
δ : Type ?u.1227
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)
rcases hs with ⟨U, ⟨haU, hUo⟩, sub : i ⁻¹' U ⊆ s⟩
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.1224
δ : Type ?u.1227
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)
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.1224
δ : Type ?u.1227
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)
refine' mem_of_superset (hUo.mem_nhds haU) _
no goals
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.1224
δ : Type ?u.1227
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)
calc
  U ⊆ closure (i '' (i ⁻¹' U)) := di.dense.subset_closure_image_preimage_of_isOpen hUo
  _ ⊆ closure (i '' s) := closure_mono (image_subset i sub)