multipliable_compl_iff — Mathlib

English

If s is a finite subset of β, then f restricted to the complement of s is multipliable if and only if f is multipliable.

Русский

Если s — конечное множество подмножеств β, то функция f, ограниченная на дополнение к s, умножаема тогда и только тогда, когда сама функция f умножаема.

LaTeX

$$$\forall s:\text{Finite}(s)\;:\; \operatorname{Multipliable}(f) \iff \operatorname{Multipliable}(f\restriction (\beta \setminus s)).$$$

Lean4

@[to_additive]
theorem multipliable_compl_iff {s : Set β} (hs : s.Finite) : Multipliable (f ∘ (↑) : ↑sᶜ → α) ↔ Multipliable f :=
  (hs.multipliable f).multipliable_compl_iff

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