of_finite — Mathlib

English

If β is finite and L has a HasSupport, then every function f: β → α is Multipliable with respect to L.

Русский

Если β конечно и L имеет HasSupport, то любая функция f: β → α мультиплируема относительно L.

LaTeX

$$$[Finite \ β] \; [L.HasSupport] \; {f: β \to α} : \text{Multipliable } f L$$$

Lean4

@[to_additive]
theorem of_finite [Finite β] [L.HasSupport] {f : β → α} : Multipliable f L :=
  multipliable_of_finite_mulSupport <| Set.finite_univ.subset (Set.subset_univ _)

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