term_⊗ₘ_ — Mathlib

English

If μ is not SFinite, then μ ⊗ₘ κ = 0 for any kernel κ; in particular, compProd_of_not_sfinite.

Русский

Если μ не SFinite, то μ ⊗ₘ κ = 0 для любого ядра κ.

LaTeX

$$$Not( SFinite(\\mu) ) \\Rightarrow \\mu \\otimes_{m} \\kappa = 0$$$

Lean4

@[inherit_doc MeasureTheory.Measure.compProd, scoped term_parser 1000]
public meta def «term_⊗ₘ_» : Lean.TrailingParserDescr✝ :=
  ParserDescr.trailingNode✝ `ProbabilityTheory.«term_⊗ₘ_» 100 100
    (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " ⊗ₘ ") (ParserDescr.cat✝ `term 101))

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