toWithTop_top — Mathlib

English

Let toWithTop be the canonical map from PartENat to the extended naturals. Then the image of the top element is the top element: toWithTop(⊤) = ⊤.

Русский

Пусть toWithTop — каноническое отображение от PartENat к расширенным неотрицательным целым, тогда образ верхнего элемента равен верхнему: toWithTop(⊤) = ⊤.

LaTeX

$$$\\\\operatorname{toWithTop}(\\\\top) = \\\\top$$$

Lean4

theorem toWithTop_top :
    have : Decidable (⊤ : PartENat).Dom := Part.noneDecidable
    toWithTop ⊤ = ⊤ :=
  rfl

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