English
Given a controlling family U with cover property, and a coherence condition hf, f is Cauchy.
Русский
Если есть контролирующая семейство U и условие совместимости hf, то f — Коши.
LaTeX
$$$(\\forall s\\in 𝓤 α)(\\exists n, U_n\\subseteq s) \\Rightarrow (\\forall N,m,n, N\\le m,N\\le n \\Rightarrow (f(m),f(n))\\in U_N) \\Rightarrow CauchySeq(f).$$$
Lean4
theorem cauchySeq_of_controlled [SemilatticeSup β] [Nonempty β] (U : β → Set (α × α)) (hU : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s)
{f : β → α} (hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N) : CauchySeq f :=
cauchySeq_iff_tendsto.2
(by
intro s hs
rw [mem_map, mem_atTop_sets]
obtain ⟨N, hN⟩ := hU s hs
refine ⟨(N, N), fun mn hmn => ?_⟩
obtain ⟨m, n⟩ := mn
exact hN (hf hmn.1 hmn.2))
