term_×ₖ_ — Mathlib

English

If η is not s-finite, then κ ×ₖ η = 0 for any κ.

Русский

Если η не s-конечное, то κ ×ₖ η = 0.

LaTeX

$$$$\\text{If } ¬\\text{IsSFiniteKernel } η, \\text{ then } κ ×ₖ η = 0.$$$$

Lean4

@[inherit_doc ProbabilityTheory.Kernel.prod, 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))

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