measurable_natCast — Mathlib

English

If α admits a natural-number cast, then for every n ∈ ℕ the constant function β → α given by n is measurable.

Русский

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

LaTeX

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

Lean4

@[measurability]
theorem measurable_natCast [NatCast α] (n : ℕ) : Measurable (n : β → α) :=
  @measurable_const α _ _ _ n

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