instOrderBot — Mathlib

English

There is a bottom kernel (zero kernel) in the pointwise order: for all a, 0 ≤ κ a.

Русский

Существует нижняя грань в частично упорядоченном пространстве ядер: для всех a выполняется 0 ≤ κ a.

LaTeX

$$$\forall a, 0 \leq \kappa a$$$

Lean4

noncomputable instance instOrderBot {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] : OrderBot (Kernel α β)
    where
  bot := 0
  bot_le κ a := by simp only [coe_zero, Pi.zero_apply, Measure.zero_le]

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