add — Mathlib

English

The sum of finite many finite kernels is finite: if κ, η are finite then κ + η is finite.

Русский

Сумма конечного числа конечных ядер конечна: κ, η — конечны, значит κ + η конечно.

LaTeX

$$$\text{IsFiniteKernel}(\kappa) \land \text{IsFiniteKernel}(\eta) \Rightarrow \text{IsFiniteKernel}(\kappa + \eta)$$$

Lean4

instance add (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKernel η] : IsFiniteKernel (κ + η) :=
  by
  refine ⟨⟨κ.bound + η.bound, ENNReal.add_lt_top.mpr ⟨κ.bound_lt_top, η.bound_lt_top⟩, fun a => ?_⟩⟩
  exact add_le_add (Kernel.measure_le_bound _ _ _) (Kernel.measure_le_bound _ _ _)

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