convolution_pos — Mathlib

English

For A,B ⊆ G finite and x ∈ G, the convolution value (A * B)(x) is positive iff x lies in the product set AB.

Русский

Для конечных A,B ⊆ G и x ∈ G значение свёртки (A * B)(x) положительно тогда и только тогда, когда x принадлежит множеству AB.

LaTeX

$$$ (A * B)(x) > 0 \iff x \in A B $$$

Lean4

@[to_additive (attr := simp) addConvolution_pos]
theorem convolution_pos : 0 < A.convolution B x ↔ x ∈ A * B := by
  aesop (add simp [convolution, Finset.Nonempty, mem_mul])

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