instBoundedGENhdsClassOrderDual

Mathlib.Topology.Order.LiminfLimsup

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

English

There is an instance turning the order dual of α into a BoundedGENhdsClass given by the original isBounded_le_nhds.

Русский

Существует инстанс, переводящий двойственную по порядку структуру α в BoundedGENhdsClass через isBounded_le_nhds.

LaTeX

$$$$ \text{BoundedGENhdsClass }(\text{OrderDual }\alpha). $$$$

Lean4

instance : BoundedGENhdsClass αᵒᵈ :=
  ⟨@isBounded_le_nhds α _ _ _⟩

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

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

Разделы

Аффилиация

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