liftBoundedOrder — Mathlib

English

If α has a bounded order and gi is a Galois insertion, then β inherits a bounded order via liftOrderTop and liftOrderBot.

Русский

Если у α есть ограниченная по порядку структура, и существует Галуа-вставка, то β наследует ограниченную по порядку структуру через поднятие верхней и нижней границы.

LaTeX

$$$$ \text{BoundedOrder}_{β} := \{ \text{top}_{β}, \text{bot}_{β}, \lor_{β}, \land_{β} \} \text{ with } \lor_{β}, \land_{β} ext{ defined via lift operations}. $$$$

Lean4

/-- Lift the top, bottom, suprema, and infima along a Galois insertion -/
abbrev liftBoundedOrder [Preorder α] [BoundedOrder α] (gi : GaloisInsertion l u) : BoundedOrder β :=
  { gi.liftOrderTop, gi.gc.liftOrderBot with }
    -- See note [reducible non-instances]

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