no goals
α : Type u_1
β : Type u_2
γ : Type ?u.27032
δ : Type ?u.27035
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
simpa [Filter.le_def] using H a