term_∥ₖ_ — Mathlib

English

The action of parallelComp on a pair (a,c) is κ(a) × η(c).

Русский

Действие parallelComp на пару (a,c) равно κ(a) × η(c).

LaTeX

$$$(\\kappa \\parallel_k \\eta)(a,c) = (\\kappa(a)) \\mathrm{prod} (\\eta(c))$$$

Lean4

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

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