mul_compl — Mathlib

English

If HasProd on s and on sᶜ hold, then HasProd on β with the combined product holds.

Русский

Если HasProd на s и на дополнении sᶜ держится, то HasProd на β с общим произведением существует.

LaTeX

$$HasProd f (a * b)$$

Lean4

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

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