measurable_intCast — Mathlib

English

If α has an integer-number cast, then for every n ∈ ℤ the constant function β → α given by n is measurable.

Русский

Если существует отображение intCast для α, то для каждого целого числа n функция β → α, принимающая постоянное значение n, измерима.

LaTeX

$$$\\forall n : \\mathbb{Z},\\ Measurable (n : \\beta \\to \\alpha)$$$

Lean4

@[measurability]
theorem measurable_intCast [IntCast α] (n : ℤ) : Measurable (n : β → α) :=
  @measurable_const α _ _ _ n

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