discard — Mathlib

English

A concise expression for deterministic kernel applied to a set: the kernel applied to a has mass concentrated at f(a).

Русский

Краткое выражение детерминированного ядра, применяемого к a; масса сосредоточена в f(a).

LaTeX

$$$\deterministic f hf(a)(s) = 1_{f(a)\in s}$$$

Lean4

/-- The Markov kernel to the `Unit` type. -/
noncomputable def discard (α : Type*) [MeasurableSpace α] : Kernel α Unit :=
  Kernel.deterministic (fun _ ↦ ()) measurable_const

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