oneLePart_def

Mathlib.Algebra.Order.Group.PosPart

URI: https://scilib.ai/kg/mathlib#Pi.oneLePart_def

English

For a family of groups, oneLePart of f equals the function i ↦ (f(i))⁺ᵐ.

Русский

Для семейства групп oneLePart f равен функции i ↦ (f(i))⁺ᵐ.

LaTeX

$$f^{+m} = \lambda i. (f(i))^{+m}$$

Lean4

@[to_additive]
theorem oneLePart_def (f : ∀ i, α i) : f⁺ᵐ = fun i ↦ (f i)⁺ᵐ :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru