Theorems · Theorem · general topology

AddGroupFilterBasis.cauchy_iff

∀ {G : Type u_1} [inst : AddCommGroup G] (B : AddGroupFilterBasis G) {F : Filter G},
  Cauchy F ↔ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U

Defined in

Mathlib.Topology.Algebra.UniformFilterBasis

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommGroup