compl_mul — Mathlib

English

Same as above: combining multiplicability on s and sᶜ yields multiplicability on whole domain.

Русский

То же самое: объединение множимости на s и sᶜ порождает множимость на β.

LaTeX

$$Multipliable f$$

Lean4

@[to_additive]
theorem compl_mul {s : Set β} (ha : HasProd (f ∘ (↑) : (sᶜ : Set β) → α) a) (hb : HasProd (f ∘ (↑) : s → α) b) :
    HasProd f (a * b) :=
  ha.mul_isCompl isCompl_compl.symm hb

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