diff --git a/src/topology/constructions.lean b/src/topology/constructions.lean
index d5dcfbaa418a0..ed8afd169447e 100644
--- a/src/topology/constructions.lean
+++ b/src/topology/constructions.lean
@@ -764,6 +764,9 @@ lemma continuous_at_subtype_coe {p : α → Prop} {a : subtype p} :
   continuous_at (coe : subtype p → α) a :=
 continuous_iff_continuous_at.mp continuous_subtype_coe _
 
+lemma subtype.dense_iff {s : set α} {t : set s} : dense t ↔ s ⊆ closure (coe '' t) :=
+by { rw [inducing_coe.dense_iff, set_coe.forall], refl }
+
 lemma map_nhds_subtype_coe_eq {a : α} (ha : p a) (h : {a | p a} ∈ 𝓝 a) :
   map (coe : subtype p → α) (𝓝 ⟨a, ha⟩) = 𝓝 a :=
 map_nhds_induced_of_mem $ by simpa only [subtype.coe_mk, subtype.range_coe] using h
diff --git a/src/topology/maps.lean b/src/topology/maps.lean
index 0ee53629c58ec..2092ab6381fe6 100644
--- a/src/topology/maps.lean
+++ b/src/topology/maps.lean
@@ -129,6 +129,10 @@ lemma inducing.is_open_iff {f : α → β} (hf : inducing f) {s : set α} :
   is_open s ↔ ∃ t, is_open t ∧ f ⁻¹' t = s :=
 by rw [hf.induced, is_open_induced_iff]
 
+lemma inducing.dense_iff {f : α → β} (hf : inducing f) {s : set α} :
+  dense s ↔ ∀ x, f x ∈ closure (f '' s) :=
+by simp only [dense, hf.closure_eq_preimage_closure_image, mem_preimage]
+
 end inducing
 
 section embedding