cauchy_iff — Mathlib

English

For a filter basis B on an additive group G, a filter F is Cauchy with respect to B if and only if F is nontrivial and for every U in B there is M in F such that any x,y in M satisfy y - x ∈ U.

Русский

Для основания фильтра B на аддитивной группе G, фильтр F является Cauchy относительно B тогда и только тогда, когда F не тривиален и для каждого U ∈ B существует M ∈ F такое, что для любых x,y ∈ M верно y - x ∈ U.

LaTeX

$$$Cauchy\,F \iff F\neq \bot \land \forall U\in B, \exists M\in F, \forall x\in M, \forall y\in M, y - x \in U$$$

Lean4

theorem cauchy_iff {F : Filter G} :
    @Cauchy G B.uniformSpace F ↔ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ᵉ (x ∈ M) (y ∈ M), y - x ∈ U :=
  by
  letI := B.uniformSpace
  haveI := B.isUniformAddGroup
  suffices F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ᵉ (x ∈ M) (y ∈ M), y - x ∈ U by
    constructor <;> rintro ⟨h', h⟩ <;> refine ⟨h', ?_⟩ <;> [rwa [← this]; rwa [this]]
  rw [uniformity_eq_comap_nhds_zero G, ← map_le_iff_le_comap]
  change Tendsto _ _ _ ↔ _
  simp [(basis_sets F).prod_self.tendsto_iff B.nhds_zero_hasBasis, @forall_swap (_ ∈ _) G]

Похожие утверждения