multipliable_of_finite_mulSupport

English

Assume L has a summation filter and mulSupport f is finite. Then f is Multipliable with respect to L.

Русский

Пусть L имеет фильтр суммирования, а mulSupport f конечно. Тогда f мультиплируема относительно L.

LaTeX

$$$[L.HasSupport] (\operatorname{mulSupport} f).\text{Finite} \Rightarrow \text{Multipliable } f L$$$

Lean4

@[to_additive]
theorem multipliable_of_finite_mulSupport [L.HasSupport] (h : (mulSupport f).Finite) : Multipliable f L := by
  apply multipliable_of_ne_finset_one (s := h.toFinset); simp

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