mul_isCompl — Mathlib

English

If s and t are complementary subsets of β, then HasProd on s and on t yields HasProd on β with product equal to the product of the two pieces.

Русский

Если s и t — несовпадающие дополнения к β, тогда HasProd на s и на t даёт HasProd на β с произведением, равным произведению частей.

LaTeX

$$HasProd (Function.comp f Subtype.val) (a * b) L$$

Lean4

@[to_additive]
theorem mul_isCompl {s t : Set β} (hs : IsCompl s t) (ha : HasProd (f ∘ (↑) : s → α) a)
    (hb : HasProd (f ∘ (↑) : t → α) b) : HasProd f (a * b) := by
  simpa [← hs.compl_eq] using (hasProd_subtype_iff_mulIndicator.1 ha).mul (hasProd_subtype_iff_mulIndicator.1 hb)

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