to_BoundedGENhdsClass

Mathlib.Topology.Order.LiminfLimsup

URI: https://scilib.ai/kg/mathlib#OrderBot.to_BoundedGENhdsClass

English

An OrderBot space has BoundGENhdsClass, via the bottom element bound.

Русский

Пространство с OrderBot обладает BoundGENhdsClass через нижнюю границу.

LaTeX

$$$ [OrderBot\; \alpha] \Rightarrow BoundGENhdsClass \alpha. $$$

Lean4

instance (priority := 100) to_BoundedGENhdsClass [OrderBot α] : BoundedGENhdsClass α :=
  ⟨fun _a ↦ isBounded_ge_of_bot⟩

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

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

Разделы

Аффилиация

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