instBot — Mathlib

English

The bottom nucleus acts as the identity on X; i.e., it maps every x to x.

Русский

Нижний нуклеус действует как тождественный на X; то есть он отправляет каждое x в x.

LaTeX

$$$\bot(x) = x$$$

Lean4

/-- The smallest nucleus is the identity. -/
instance instBot : OrderBot (Nucleus X) where
  bot.toFun x := x
  bot.idempotent' := by simp
  bot.le_apply' := by simp
  bot.map_inf' := by simp
  bot_le n _ := n.le_apply

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