α : Type u_1
β : Type u_2
γ : Type ?u.2172
δ : Type ?u.2175
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di✝ di : DenseInducing i
s : Set α
H : Dense (i '' s)
x : α
⊢ x ∈ closure s
α : Type u_1
β : Type u_2
γ : Type ?u.2172
δ : Type ?u.2175
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di✝ di : DenseInducing i
s : Set α
⊢ Dense (i '' s) ↔ Dense s
refine' ⟨fun H x => _, di.dense.dense_image di.continuous⟩
α : Type u_1
β : Type u_2
γ : Type ?u.2172
δ : Type ?u.2175
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di✝ di : DenseInducing i
s : Set α
H : Dense (i '' s)
x : α
⊢ x ∈ univ
α : Type u_1
β : Type u_2
γ : Type ?u.2172
δ : Type ?u.2175
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di✝ di : DenseInducing i
s : Set α
H : Dense (i '' s)
x : α
⊢ x ∈ closure s
rw [di.toInducing.closure_eq_preimage_closure_image, H.closure_eq, preimage_univ]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.2172
δ : Type ?u.2175
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di✝ di : DenseInducing i
s : Set α
H : Dense (i '' s)
x : α
⊢ x ∈ univ
trivial