instBoundedOrder — Mathlib

English

CompactOpens α forms a bounded order under inclusion, with top = univ and bottom = empty set.

Русский

CompactOpens(α) образует ограниченное множество по включению; верхняя и нижняя границы соответствуют univ и пустому множеству.

LaTeX

$$$\mathrm{CompactOpens}(\alpha)\text{ is a bounded order with }\top=\mathrm{univ},\ \bot=\varnothing$$$

Lean4

instance instBoundedOrder : BoundedOrder (CompactOpens α) :=
  BoundedOrder.lift ((↑) : _ → Set α) (fun _ _ => id) coe_top coe_bot

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