English
Let l be a list and fs a family of lists. An element f belongs to the dependent product pi l fs iff, for every i in l, f i hi lies in fs i.
Русский
Пусть l — список, fs — зависимая семейство списков. Элемент f принадлежит зависимому произведению pi l fs тогда и только тогда, когда для каждого i∈l элемент f i hi принадлежит fs i.
LaTeX
$$$(f ∈ \pi l fs) \iff (\forall i (hi : i \in l), f i hi \in fs i)$$$
Lean4
theorem mem_pi {l : List ι} (fs : ∀ i, List (α i)) (f : ∀ i ∈ l, α i) :
(f ∈ pi l fs) ↔ (∀ i (hi : i ∈ l), f i hi ∈ fs i) := by simpa [Multiset.pi_coe] using Multiset.mem_pi ↑l (fs ·) f
