instBoundedOrder

Mathlib.Topology.Sets.Order

URI: https://scilib.ai/kg/mathlib#ClopenUpperSet.instBoundedOrder

English

The poset ClopenUpperSet α is a bounded order, with top and bottom elements.

Русский

Порядок ClopenUpperSet α является ограниченным по верхней и нижней границе.

LaTeX

$$$\\\\text{instBoundedOrder}: \\\\text{BoundedOrder}(ClopenUpperSet(\\\\alpha))$$$

Lean4

instance : BoundedOrder (ClopenUpperSet α) :=
  BoundedOrder.lift ((↑) : _ → Set α) (fun _ _ => id) rfl rfl

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

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

Разделы

Аффилиация

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