multipliable_compl_iff — Mathlib

English

If s is a set and f restricted to s is Multipliable, then Multipliable of f restricted to the complement is equivalent to Multipliable f.

Русский

Если множество s и функция f на s Multipliable, то Multipliable на дополнении эквивалентно Multipliable f.

LaTeX

$$Multipliable (f ∘ (↑) : s → α) → Iff (Multipliable (f ∘ (↑) : ↑sᶜ → α)) (Multipliable f)$$

Lean4

@[to_additive]
theorem multipliable_compl_iff {s : Set β} (hf : Multipliable (f ∘ (↑) : s → α)) :
    Multipliable (f ∘ (↑) : ↑sᶜ → α) ↔ Multipliable f
    where
  mp := fun ⟨_, ha⟩ ↦ (hf.hasProd.hasProd_compl_iff.1 ha).multipliable
  mpr := fun ⟨_, ha⟩ ↦ (hf.hasProd.hasProd_iff_compl.1 ha).multipliable

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