hasProd_singleton — Mathlib

English

For any m ∈ β and any f: β → α, HasProd on the singleton {m} (via restriction) equals f(m); i.e., the product over a single index is just the value at that index.

Русский

Для любого m∈β и функции f: β→α, HasProd на одноэлементном множестве {m} равен f(m); произведение по единому индексу равно значению в этом индексе.

LaTeX

$$$\text{HasProd } ((\{ m \} : Set \beta)\restrict f) (f m)$$$

Lean4

@[to_additive (attr := simp)]
theorem hasProd_singleton (m : β) (f : β → α) : HasProd (({ m } : Set β).restrict f) (f m) :=
  hasProd_unique (Set.restrict { m } f)

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