comapRight — Mathlib

English

If κ is a finite kernel, then comapRight κ hf is a finite kernel with the same bound.

Русский

Если κ — конечное ядро, то comapRight κ hf — конечное ядро с тем же верхним пределом.

LaTeX

$$$\\text{IsFiniteKernel}(\\kappa\\, hf)$$$

Lean4

instance comapRight (κ : Kernel α β) [IsFiniteKernel κ] (hf : MeasurableEmbedding f) :
    IsFiniteKernel (comapRight κ hf) :=
  by
  refine ⟨⟨κ.bound, κ.bound_lt_top, fun a => ?_⟩⟩
  rw [comapRight_apply' κ hf a .univ]
  exact measure_le_bound κ a _

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