mem_fintype_prod — Mathlib

English

For a finite index type, membership in the product equals the existence of pointwise choices from each set with the overall product equal to the target.

Русский

Для конечного индекса существование выборок из каждого множества обеспечивает принадлежность произведению.

LaTeX

$$a ∈ ∏ i, f i ↔ ∃ g : i → α, ∀ i, g i ∈ f i ∧ ∏ i, g i = a$$

Lean4

/-- A version of `Set.mem_finset_prod` with a simpler RHS for products over a Fintype. -/
@[to_additive /-- A version of `Set.mem_finset_sum` with a simpler RHS for sums over a Fintype. -/
    ]
theorem mem_fintype_prod [Fintype ι] (f : ι → Set α) (a : α) :
    (a ∈ ∏ i, f i) ↔ ∃ (g : ι → α) (_ : ∀ i, g i ∈ f i), ∏ i, g i = a :=
  by
  rw [mem_finset_prod]
  simp

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