multipliable_apply — Mathlib

English

If f: γ → C(α, β) is multipliable with respect to a summation filter L, then for all x ∈ α, the family f(i)(x) is multipliable with respect to L.

Русский

Если f: γ → C(α, β) есть мультиплицируемость, то для каждой точки x произведение в значениях f(i)(x) тоже мультиплифицируемо по L.

LaTeX

$$$\forall x:\; Multipliable (f i)\, x\; L$$$

Lean4

@[to_additive]
theorem multipliable_apply [CommMonoid β] [ContinuousMul β] {γ : Type*} {f : γ → C(α, β)} {L : SummationFilter γ}
    (hf : Multipliable f L) (x : α) : Multipliable (fun i : γ ↦ f i x) L :=
  (hasProd_apply hf.hasProd x).multipliable

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