compProd_congr — Mathlib

English

If two kernels κ and η are almost everywhere equal with respect to μ, then μ ⊗ₘ κ = μ ⊗ₘ η.

Русский

Если два ядра κ и η равны почти всюду по отношению к μ, то μ ⊗ₘ κ = μ ⊗ₘ η.

LaTeX

$$$[\\mathrm{IsSFiniteKernel}\\; κ] [\\mathrm{IsSFiniteKernel}\\; η] (h : κ =^\\mu\\! η) \\Rightarrow μ ⊗_m κ = μ ⊗_m η$$$

Lean4

theorem compProd_congr [IsSFiniteKernel κ] [IsSFiniteKernel η] (h : κ =ᵐ[μ] η) : μ ⊗ₘ κ = μ ⊗ₘ η :=
  by
  rw [compProd, compProd]
  congr 1
  refine Kernel.compProd_congr ?_
  simpa

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