bddAbove_iff_subset_Iic

Mathlib.Order.Bounds.Basic

URI: https://scilib.ai/kg/mathlib#bddAbove_iff_subset_Iic

English

The set s is bounded above if and only if there exists a such that s ⊆ Iic(a).

Русский

Множество s ограничено сверху тогда и только тогда, когда существует a, чтобы s ⊆ Iic(a).

LaTeX

$$$\mathrm{bddAbove}(s) \iff \exists a, \ s \subseteq \mathrm{Iic}(a).$$$

Lean4

theorem bddAbove_iff_subset_Iic : BddAbove s ↔ ∃ a, s ⊆ Iic a :=
  Iff.rfl

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

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

Разделы

Аффилиация

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