instIsFiniteKernelBoolBoolKernelOfIsFiniteMeasure

English

A kernel from Bool to α is determined by its values at false and at true: κ = boolKernel(κ(false), κ(true)).

Русский

Ядро, определяющее отображение Bool → α, задаётся значениями на false и true: κ = boolKernel(κ(false), κ(true)).

LaTeX

$$$\\kappa = \\text{boolKernel}(\\kappa(\\text{false}), \\kappa(\\text{true}))$$$

Lean4

instance [IsFiniteMeasure μ] [IsFiniteMeasure ν] : IsFiniteKernel (boolKernel μ ν) :=
  ⟨max (μ .univ) (ν .univ), max_lt (measure_lt_top _ _) (measure_lt_top _ _), fun b ↦ by cases b <;> simp⟩

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