isBounded_compl_iff

Mathlib.Topology.Bornology.Basic

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

English

IsCobounded of the complement of s is equivalent to IsBounded s.

Русский

IsCobounded для дополнения к s эквивалентно IsBounded s.

LaTeX

$$$IsCobounded (s^c) \\Leftrightarrow IsBounded s$$$

Lean4

@[simp]
theorem isBounded_compl_iff : IsBounded sᶜ ↔ IsCobounded s := by rw [isBounded_def, isCobounded_def, compl_compl]

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

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

Разделы

Аффилиация

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