nonempty_of_not_isBounded

Mathlib.Topology.Bornology.Basic

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

English

If a set is not bounded, then it is nonempty.

Русский

Если множество не ограничено, значит оно непустое.

LaTeX

$$$\\lnot IsBounded s \\Rightarrow s.Nonempty$$$

Lean4

theorem nonempty_of_not_isBounded (h : ¬IsBounded s) : s.Nonempty :=
  by
  rw [nonempty_iff_ne_empty]
  rintro rfl
  exact h isBounded_empty

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

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

Разделы

Аффилиация

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