infConvergenceClass'

Mathlib.Topology.Order.MonotoneConvergence

URI: https://scilib.ai/kg/mathlib#Pi.infConvergenceClass'

← MathLib Explorer

English

Variant of Pi InfConvergence for a generalized Pi-space.

Русский

Вариант утверждения о инфиничестве для пространства Пи.

LaTeX

$$$ \text{InfConvergenceClass}(\forall i, \alpha(i)) $$$

Lean4

instance infConvergenceClass' {ι : Type*} [Preorder α] [TopologicalSpace α] [InfConvergenceClass α] :
    InfConvergenceClass (ι → α) :=
  Pi.infConvergenceClass

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

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

Разделы

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

Аффилиация

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