instAddLeftMono — Mathlib

English

Addition of kernels is monotone in the left argument: if κ ≤ κ' then κ + η ≤ κ' + η.

Русский

Сложение ядер монотонно по левому аргументу: если κ ≤ κ', то κ + η ≤ κ' + η.

LaTeX

$$$\kappa \leq \kappa' \; \Rightarrow \; \kappa + \eta \leq \kappa' + \eta$$$

Lean4

instance {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] : AddLeftMono (Kernel α β) :=
  ⟨fun _ _ _ hμ a ↦ add_le_add_left (hμ a) _⟩

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