abs_apply — Mathlib

English

For a family of abelian groups α i indexed by ι, the pointwise absolute value of a function f : ∀ i, α i satisfies (|f|) i = |f i| for every i ∈ ι.

Русский

Для семейства групп с индексами ι функцией f : ∀ i, α i определено точечное модуль: (|f|) i = |f(i)| для каждого i.

LaTeX

$$$\forall i, \ |f| i = |f i|$$$

Lean4

@[simp]
theorem abs_apply (f : ∀ i, α i) (i : ι) : |f| i = |f i| :=
  rfl

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