Theorems · Theorem · general topology

Metric.eventually_nhds_iff

∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {p : α → Prop},
  (∀ᶠ (y : α) in nhds x, p y) ↔ ∃ ε > 0, ∀ ⦃y : α⦄, dist y x < ε → p y

Defined in

Mathlib.Topology.MetricSpace.Pseudo.Defs

Cited by

5 results in Mathlib

Foundations

Depth 116 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoMetricSpace