pi

Mathlib.Topology.UniformSpace.Pi

URI: https://scilib.ai/kg/mathlib#Cauchy.pi

← MathLib Explorer

English

If each α_i is a complete space, then the product space ∀ i, α_i is complete.

Русский

Если каждое пространство α_i полно (complete), то произведение ∀ i, α_i полно.

LaTeX

$$$\\text{CompleteSpace} (\\forall i, \\alpha_i)$$$

Lean4

theorem pi [Nonempty ι] {l : ∀ i, Filter (α i)} (hl : ∀ i, Cauchy (l i)) : Cauchy (Filter.pi l) :=
  by
  have := fun i ↦ (hl i).1
  simpa [cauchy_pi_iff]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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