seq_is_cauchySeq

Mathlib.Topology.UniformSpace.Cauchy

URI: https://scilib.ai/kg/mathlib#SequentiallyComplete.seq_is_cauchySeq

English

Under a suitable control (U_le), the sequence seq hf U_mem is Cauchy.

Русский

При наличии подходящего контроля (U_le) последовательность seq hf U_mem является Коши.

LaTeX

$$$\text{CauchySeq}(\text{SequentiallyComplete.seq}(hf,U_{mem}))$$$

Lean4

theorem seq_is_cauchySeq (U_le : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s) : CauchySeq <| seq hf U_mem :=
  cauchySeq_of_controlled U U_le <| seq_pair_mem hf U_mem

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru