mem_pi — Mathlib

English

An element f of s.π t is precisely a function on s such that for every a ∈ s, f(a) ∈ t(a).

Русский

Элемент f ∈ s.π t равен функции на s такая что для каждого a ∈ s имеет место f(a) ∈ t(a).

LaTeX

$$$ f \\in s.\\pi t \\iff \\forall a (h:\\, a \\in s),\\ f(a,h) \\in t(a). $$$

Lean4

@[simp]
theorem mem_pi {s : Finset α} {t : ∀ a, Finset (β a)} {f : ∀ a ∈ s, β a} :
    f ∈ s.pi t ↔ ∀ (a) (h : a ∈ s), f a h ∈ t a :=
  Multiset.mem_pi _ _ _

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