α : Type u
β : Type v
X : Type ?u.28215
inst✝ : PseudoEMetricSpace α
f : Filter α
⊢ Cauchy f ↔ NeBot f ∧ ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, t ∈ f ∧ ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → edist x y < ε
α : Type u
β : Type v
X : Type ?u.28215
inst✝ : PseudoEMetricSpace α
f : Filter α
⊢ Cauchy f ↔ f ≠ ⊥ ∧ ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, t ∈ f ∧ ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → edist x y < ε
rw [← neBot_iff]
no goals
α : Type u
β : Type v
X : Type ?u.28215
inst✝ : PseudoEMetricSpace α
f : Filter α
⊢ Cauchy f ↔ NeBot f ∧ ∀ (ε : ℝ≥0∞), ε > 0 → ∃ t, t ∈ f ∧ ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → edist x y < ε
exact uniformity_basis_edist.cauchy_iff