oneLePart_apply — Mathlib

English

In a family of groups indexed by i, the positive part applied pointwise yields (f⁺ᵐ)(i) = (f(i))⁺ᵐ.

Русский

В семействе групп, индексированном по i, положительная часть применяется по каждому индексу: (f⁺ᵐ)(i) = (f(i))⁺ᵐ.

LaTeX

$$f^{+m}(i) = (f(i))^{+m}$$

Lean4

@[to_additive (attr := simp)]
theorem oneLePart_apply (f : ∀ i, α i) (i : ι) : f⁺ᵐ i = (f i)⁺ᵐ :=
  rfl

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