multipliable — Mathlib

English

If the set s is finite, then Multipliable (f restricted to s) holds; equivalently, finite-domain products converge as expected.

Русский

Если множество s конечное, то Multipliable (f на s) выполняется; эквивалентно сходятся конечные произведения.

LaTeX

$$$s\ Fintie \Rightarrow \text{Multipliable } (f \circ (↑): s \to α)$$$

Lean4

@[to_additive]
protected theorem multipliable {s : Set β} (hs : s.Finite) (f : β → α) : Multipliable (f ∘ (↑) : s → α) :=
  by
  have := hs.toFinset.multipliable f
  rwa [hs.coe_toFinset] at this

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