English
Let t be a family of finite subsets t(a) ⊆ δ(a) indexed by a in α. The set of all functions f with f(a) ∈ t(a) for every a is exactly the dependent product ∏a t(a). Equivalently, the piFinset corresponding to t, viewed as a set, coincides with the pi-set built from t.
Русский
Пусть t задаёт семейство конечных множеств t(a) ⊆ δ(a) индексируемых по a в α. Все функции f, удовлетворяющие f(a) ∈ t(a) для каждого a, образуют точное декартово произведение ∏a t(a). Аналогично, множество piFinset, рассматриваемое как множество, совпадает с произведением по a от t(a).
LaTeX
$$$\\{ f : \\prod_{a \\in \\alpha} \\delta(a) \\mid \\forall a \\in \\alpha,\\, f(a) \\in t(a) \\} = \\prod_{a \\in \\alpha} t(a).$$$
Lean4
@[simp]
theorem coe_piFinset (t : ∀ a, Finset (δ a)) : (piFinset t : Set (∀ a, δ a)) = Set.pi Set.univ fun a => t a :=
Set.ext fun x => by
rw [Set.mem_univ_pi]
exact Fintype.mem_piFinset
