setSeq_mem

Mathlib.Topology.UniformSpace.Cauchy

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

English

Each setSeq n belongs to the Cauchy filter f.

Русский

Каждоe множество setSeq(n) принадлежит фильтру f.

LaTeX

$$$setSeq\,hf\,U_{mem}\,n \in f$$$

Lean4

theorem setSeq_mem (n : ℕ) : setSeq hf U_mem n ∈ f :=
  (biInter_mem (finite_le_nat n)).2 fun m _ => (setSeqAux hf U_mem m).2.1

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

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

Разделы

Аффилиация

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