coeFn_one_eq — Mathlib

English

Let μ be a measure with μ ≠ 0 and β a type with a multiplicative identity. The constant function 1, viewed as an almost everywhere equal function α →ₘ[μ] β, takes the value 1 at every point x ∈ α.

Русский

Пусть μ — мера с μ ≠ 0 и β — множество с тождественным элементом умножения. Константная функция 1, рассмотренная как почти всюду равная функция α →ₘ[μ] β, принимает значение 1 в каждой точке x ∈ α.

LaTeX

$$$\forall x: \alpha,\ (1 : \alpha \to_{\mu} \beta)\,x = 1$$$

Lean4

@[to_additive (attr := simp)]
theorem coeFn_one_eq [NeZero μ] [One β] {x : α} : (1 : α →ₘ[μ] β) x = 1 :=
  coeFn_const_eq ..

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