multipliable_subtype_and_compl — Mathlib

English

For any f: β → α and any subset s ⊆ β, f is Multipliable on β if and only if both its restrictions to s and to the complement of s are Multipliable.

Русский

Для любой f: β → α и подмножества s ⊆ β функция f является суммируемой на β тогда и только тогда, когда обе её части: ограничение на s и ограничение на комплемент s, суммируемы.

LaTeX

$$$$\\big( \\text{Multipliable}(f|_s) \\land \\text{Multipliable}(f|_{\\beta\\setminus s}) \\big) \\iff \\text{Multipliable}(f).$$$$

Lean4

@[to_additive]
theorem multipliable_subtype_and_compl {s : Set β} :
    ((Multipliable fun x : s ↦ f x) ∧ Multipliable fun x : ↑sᶜ ↦ f x) ↔ Multipliable f :=
  ⟨and_imp.2 Multipliable.mul_compl, fun h ↦ ⟨h.subtype s, h.subtype sᶜ⟩⟩

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