English
For a filter F on R, F is Cauchy with respect to the valuation topology iff F ≠ ∅ and for every γ ∈ Γ₀ˣ there exists M ∈ F such that ∀ x,y ∈ M, v(y−x) < γ.
Русский
Фильтр F на R является составным по топологии оценки тогда и только тогда, когда F не пуст и для каждого γ ∈ Γ₀ˣ существует M ∈ F, такое, что для любых x,y ∈ M выполнено v(y−x) < γ.
LaTeX
$$$\text{Cauchy}(F) \iff F \neq \bot \land \forall \gamma \in Γ_0^{\times}, \exists M \in F, \forall x,y \in M, v(y-x) < \gamma$$$
Lean4
theorem cauchy_iff {F : Filter R} : Cauchy F ↔ F.NeBot ∧ ∀ γ : Γ₀ˣ, ∃ M ∈ F, ∀ᵉ (x ∈ M) (y ∈ M), (v (y - x) : Γ₀) < γ :=
by
rw [toUniformSpace_eq, AddGroupFilterBasis.cauchy_iff]
apply and_congr Iff.rfl
simp_rw [Valued.v.subgroups_basis.mem_addGroupFilterBasis_iff]
constructor
· intro h γ
exact h _ (Valued.v.subgroups_basis.mem_addGroupFilterBasis _)
· rintro h - ⟨γ, rfl⟩
exact h γ
