instOrderBot

Mathlib.Topology.Sets.Compacts

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.Compacts.instOrderBot

English

There is a bottom element for the order on compact subsets, consistent with the earlier Bottom instance.

Русский

Существует нижняя граница по порядку на компакте, согласующаяся с ранее установленной нижней гранью.

LaTeX

$$$[OrderBot]\; (Compacts\,\alpha)$$$

Lean4

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

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

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

Разделы

Аффилиация

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