coeFn_const — Mathlib

English

The constant-valued function class corresponding to a fixed b ∈ β is the ae-equivalence class of the function that maps every x to b.

Русский

Класс ae-эквивалентности константной функции, соответствующий фиксированному b ∈ β, есть ae-эквивалентность функции, отправляющей каждый x в b.

LaTeX

$$$\operatorname{const}(b) = mk (\lambda x, b) aestronglyMeasurable_const$$$

Lean4

theorem coeFn_const (b : β) : (const α b : α →ₘ[μ] β) =ᵐ[μ] Function.const α b :=
  coeFn_mk _ _

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