const — Mathlib

English

The constant-one element in the ae-equivalence world corresponds to the constant function 1, up to almost-everywhere equality.

Русский

Единичный элемент в ae-эквивалентностях соответствует константной функции 1 почти везде равной.

LaTeX

$$$(1 : α \to_μ β) = \text{const}(1)$ a.e.$$

Lean4

/-- The equivalence class of a constant function: `[fun _ : α => b]`, based on the equivalence
relation of being almost everywhere equal -/
def const (b : β) : α →ₘ[μ] β :=
  mk (fun _ : α ↦ b) aestronglyMeasurable_const

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