supConvergenceClass'

Mathlib.Topology.Order.MonotoneConvergence

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

← MathLib Explorer

English

Variant of Pi SupConvergence for a generalized Pi-space.

Русский

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

LaTeX

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

Lean4

instance supConvergenceClass' {ι : Type*} [Preorder α] [TopologicalSpace α] [SupConvergenceClass α] :
    SupConvergenceClass (ι → α) :=
  supConvergenceClass

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

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

Разделы

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

Аффилиация

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