conjneg_prod — Mathlib

English

Let f_i : G → R be a family of functions and s a finite index set. The operation conjneg distributes over finite products: the conjneg of the product equals the product of the conjneg’s.

Русский

Пусть f_i : G → R задаются для i в конечном множестве s. Операция conjneg распределяется по конечным произведениям: conjneg(∏_{i∈s} f_i) = ∏_{i∈s} conjneg(f_i).

LaTeX

$$$\operatorname{conjneg}\left(\prod_{i \in s} f_i\right) = \prod_{i \in s} \operatorname{conjneg}(f_i)$$$

Lean4

@[simp]
theorem conjneg_prod (s : Finset ι) (f : ι → G → R) : conjneg (∏ i ∈ s, f i) = ∏ i ∈ s, conjneg (f i) := by ext; simp

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