multipliable — Mathlib

English

For a family f: ι → ∀x, Xx, Multipliable f L holds if and only if for all x, Multipliable (fun i => f i x) L.

Русский

Для семейства f: ι → ∀x, Xx верно, что f множимо по L тогда и только тогда, когда для каждого x выполняется множимость по i.

LaTeX

$$$\\operatorname{Multipliable} f L \\iff \\forall x, \\operatorname{Multipliable}(\\lambda i, f i x) L$$$

Lean4

@[to_additive]
theorem multipliable {f : ι → ∀ x, X x} : Multipliable f L ↔ ∀ x, Multipliable (fun i ↦ f i x) L := by
  simp only [Multipliable, Pi.hasProd, Classical.skolem]

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