English
Same as mem_sum: a ∈ ∑ i ∈ s, m i ↔ ∃ i ∈ s, a ∈ m i.
Русский
То же, что и mem_sum: a ∈ ∑ i ∈ s, m i ↔ ∃ i ∈ s, a ∈ m i.
LaTeX
$$$$ a \\in \\sum_{i\\in s} m(i) \\iff \\exists i\\in s, a\\in m(i). $$$$
Lean4
/-- `∏ x ∈ s, f x` is the product of `f x` as `x` ranges over the elements of the finite set `s`.
When the index type is a `Fintype`, the notation `∏ x, f x`, is a shorthand for
`∏ x ∈ Finset.univ, f x`. -/
@[to_additive /-- `∑ x ∈ s, f x` is the sum of `f x` as `x` ranges over the elements
of the finite set `s`.
When the index type is a `Fintype`, the notation `∑ x, f x`, is a shorthand for
`∑ x ∈ Finset.univ, f x`. -/
]
protected def prod [CommMonoid M] (s : Finset ι) (f : ι → M) : M :=
(s.1.map f).prod
