one_toGerm — Mathlib

English

The germ of the constant function 1 is itself, i.e., the germ representation of 1 in the ae-equivalent function space equals 1.

Русский

Герма константной функции 1 равна самой 1, то есть герма-репрезентация 1 в пространстве эквивалентностей почти всюду равна 1.

LaTeX

$$$ (1 : α \to_{\mu} β).toGerm = 1 $$$

Lean4

@[to_additive (attr := simp)]
theorem one_toGerm [One β] : (1 : α →ₘ[μ] β).toGerm = 1 :=
  rfl

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