ext_bot — Mathlib

English

The OrderTop structure on α is a Subsingleton; any two such structures coincide.

Русский

Структура OrderTop на α является Subsingleton; любые две такие структуры совпадают.

LaTeX

$$$\forall \alpha, Subsingleton (OrderTop \alpha)$$$

Lean4

theorem ext_bot {α} {hA : PartialOrder α} (A : OrderBot α) {hB : PartialOrder α} (B : OrderBot α)
    (H :
      ∀ x y : α,
        (haveI := hA;
          x ≤ y) ↔
          x ≤ y) :
    (@Bot.bot α (@OrderBot.toBot α hA.toLE A)) = (@Bot.bot α (@OrderBot.toBot α hB.toLE B)) :=
  by
  cases PartialOrder.ext H
  apply bot_unique
  exact @bot_le _ _ A _

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