hasProd_iff_compl — Mathlib

English

For any s, HasProd f a2 holds if and only if HasProd (f restricted to the complement) equals a2 / a1, given that HasProd on s has value a1.

Русский

Для любого s: HasProd f a2 эквивалентно HasProd (f ограниченный до дополнения) и a2 / a1 при условии HasProd на s имеет значение a1.

LaTeX

$$HasProd (f ∘ (↑) : s → α) a1 → HasProd f a2 ↔ HasProd (f ∘ (↑) : ↑sᶜ → α) (a2 / a1)$$

Lean4

@[to_additive]
theorem hasProd_iff_compl {s : Set β} (hf : HasProd (f ∘ (↑) : s → α) a₁) :
    HasProd f a₂ ↔ HasProd (f ∘ (↑) : ↑sᶜ → α) (a₂ / a₁) :=
  Iff.symm <| hf.hasProd_compl_iff.trans <| by rw [mul_div_cancel]

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