Point close to the frontier

Stream: Is there code for X?

[Yaël Dillies]

This is probably very easy, but I can't find it.

import topology.metric_space.basic

variables {α : Type*} [metric_space α] {s : set α} {x : α} {ε : ℝ}

example (hx : x ∈ frontier s) (hε : 0 < ε) : ∃ z ∈ s, dist x z < ε := sorry

[Anatole Dedecker]

docs#frontier_subset_closure and docs#metric.mem_closure_iff sould work

[Anatole Dedecker]

I guess we could add a metric.mem_frontier_iffsaying that x ∈ frontier s ↔ ∀ ε > 0, (∃ y ∈ s, dist x y < ε) ∧ (∃ z ∈ sᶜ, dist x z < ε)

[Yaël Dillies]

No need for a new lemma, I was just having a small brain moment.