instOrderBot — Mathlib

English

There exists a bottom element in the lattice of sSupHom α β, given by the constant map sending every input to ⊥ in β.

Русский

В решётке отображений, сохраняющих верхние пределы, существует нижний элемент — константное отображение, посылающее каждый аргумент в ⊥ β.

LaTeX

$$$\bot_{sSupHom(\alpha,\beta)} \,: a \mapsto \bot_β$$$

Lean4

instance : OrderBot (sSupHom α β) where
  bot := ⊥
  bot_le := fun _ _ ↦ OrderBot.bot_le _

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