instOrderBot — Mathlib

English

CompactOpens α admits a bottom element making it an ordered bottom lattice with the coercion to sets preserving order.

Русский

CompactOpens α образует частично упорядкованную матрицу снизу с нижним элементом; отображение к множествам сохраняет порядок.

LaTeX

$$$\text{OrderBot}(\text{CompactOpens } α)$$$

Lean4

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

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