isCobounded_bot

Mathlib.Order.Filter.IsBounded

URI: https://scilib.ai/kg/mathlib#Filter.isCobounded_bot

English

IsCobounded r ⊥ is equivalent to there exists a bound b such that r b x holds for all x.

Русский

IsCobounded r ⊥ эквивалентно существованию границы b, для которой r b x выполняется для всех x.

LaTeX

$$$IsCobounded\ r \bot \ \Leftrightarrow\ \exists b, \forall x, r\ b\ x.$$$

Lean4

theorem isCobounded_bot : IsCobounded r ⊥ ↔ ∃ b, ∀ x, r b x := by simp [IsCobounded]

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

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

Разделы

Аффилиация

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