ext_top — Mathlib

English

In the dual order, the bottom element maps to the top of the original order: ⊥ in the dual corresponds to ⊤ in the original.

Русский

В двойственном порядке нижний элемент соответствует верхнему в исходном порядке: ⊥ в двойственном порядке соответствует ⊤ в исходном.

LaTeX

$$$\operatorname{ofDual}(\bot) = \top$$$

Lean4

theorem ext_top {α} {hA : PartialOrder α} (A : OrderTop α) {hB : PartialOrder α} (B : OrderTop α)
    (H :
      ∀ x y : α,
        (haveI := hA;
          x ≤ y) ↔
          x ≤ y) :
    (@Top.top α (@OrderTop.toTop α hA.toLE A)) = (@Top.top α (@OrderTop.toTop α hB.toLE B)) :=
  by
  cases PartialOrder.ext H
  apply top_unique
  exact @le_top _ _ A _

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