instOrderBot — Mathlib

English

There exists a bottom element in the poset of seminorms, namely the zero seminorm. This bottom seminorm is ≤ every seminorm.

Русский

Существует нижний элемент в частично упорядоченном множестве семинорм; это нулевой семинорм. Он не превосходит любую семинорму.

LaTeX

$$$\bot = 0$$$

Lean4

instance instOrderBot : OrderBot (Seminorm 𝕜 E) where
  bot := 0
  bot_le := apply_nonneg

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