instNonemptySubtypeIsMarkovKernel

English

If β is nonempty, there exists a kernel κ of type { κ : Kernel α β // IsMarkovKernel κ }. In particular, Kernel.const with dirac measure provides such an example.

Русский

Если β ненулевой, то существует ядро κ в виде подтипа { κ : Kernel α β // IsMarkovKernel κ }. Например, Kernel.const с мерой Дирака удовлетворяет условию.

LaTeX

$$$\exists κ \in \{\kappa: Kernel \alpha \beta \mid IsMarkovKernel(\kappa)\}$$$

Lean4

instance [Nonempty β] : Nonempty { κ : Kernel α β // IsMarkovKernel κ } :=
  nonempty_subtype.2 ⟨Kernel.const _ (Measure.dirac Classical.ofNonempty), inferInstance⟩

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