boundedOrder — Mathlib

English

Regular α carries a natural bounded-order structure transported from α via the embedding; bottom and top come from ⊥ and ⊤ of α.

Русский

Regular α обладает естественной структурой ограниченного упорядочения, перенесённой из α через вложение; ⊥ и ⊤ соответствуют ⊥ и ⊤ α.

LaTeX

$$$ \forall a,b \in \mathrm{Regular}(\alpha),\ a \le_{\mathrm{Reg}} b \iff a \le b \text{ in } \alpha,\quad \bot_{\mathrm{Reg}} = \bot,\ \top_{\mathrm{Reg}} = \top.$$$

Lean4

instance boundedOrder : BoundedOrder (Regular α) :=
  BoundedOrder.lift ((↑) : Regular α → α) (fun _ _ => id) coe_top coe_bot

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