IsCobounded

Mathlib.Topology.Bornology.Basic

URI: https://scilib.ai/kg/mathlib#Bornology.IsCobounded

← MathLib Explorer

English

IsCobounded s means s is a member of the cobounded filter on α.

Русский

IsCobounded s означает, что s принадлежит фильтру кобboundeds на α.

LaTeX

$$$IsCobounded s \\equiv s \\in cobounded \\alpha$$$

Lean4

/-- `IsCobounded` is the predicate that `s` is in the filter of cobounded sets in the ambient
bornology on `α` -/
def IsCobounded [Bornology α] (s : Set α) : Prop :=
  s ∈ cobounded α

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

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

Разделы

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

Аффилиация

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