instIsFiniteMeasureBindCoeKernelOfIsFiniteKernel

English

If μ is a finite measure on α and κ is a finite kernel α → β, then the composition κ ∘ₘ μ is a finite measure on α × β.

Русский

Если μ — конечная мера на α и κ — конечное ядро α → β, тогда композиция κ ∘ₘ μ — конечная мера на α × β.

LaTeX

$$$( \mu \text{ finite} ) \\land ( \\kappa \text{ finite kernel} ) \\Rightarrow \\text{Fin}( \\kappa \\circ_{m} \\mu )$$$

Lean4

instance [IsFiniteMeasure μ] [IsFiniteKernel κ] : IsFiniteMeasure (κ ∘ₘ μ) := by rw [← snd_compProd]; infer_instance

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