piecewise — Mathlib

English

If κ and η are finite kernels, then the piecewise kernel is finite with bound max(κ.bound, η.bound).

Русский

Если κ и η конечны, то piecewise κ η конечна и имеет верхнюю границу max(κ.bound, η.bound).

LaTeX

$$$\\text{IsFiniteKernel}(\\text{piecewise}(hs,\\kappa,\\eta))$ with bound $\\max(\\kappa.bound, \\eta.bound)$$$

Lean4

instance piecewise [IsFiniteKernel κ] [IsFiniteKernel η] : IsFiniteKernel (piecewise hs κ η) :=
  by
  refine ⟨⟨max κ.bound η.bound, max_lt κ.bound_lt_top η.bound_lt_top, fun a => ?_⟩⟩
  rw [piecewise_apply']
  exact (ite_le_sup _ _ _).trans (sup_le_sup (measure_le_bound _ _ _) (measure_le_bound _ _ _))

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