mem_pi_toList — Mathlib

English

For xs and a suitable f, the dependent function f belongs to the dependent product of lists, i.e., f ∈ ∏ a∈xs toList(β a).

Русский

Для xs и подходящей функции f, зависимая функция f принадлежит зависимому произведению списков.

LaTeX

$$$ f \\in \\prod_{a \\in xs} \\mathrm{toList}(\\\\beta a). $$$

Lean4

theorem mem_pi_toList (xs : List α) (f : ∀ a, a ∈ xs → β a) : f ∈ pi xs fun x => toList (β x) :=
  (mem_pi _ _).mpr fun _ _ ↦ mem_toList _

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