mem_pi — Mathlib

English

An element g belongs to f.pi if and only if for every i, g(i) belongs to f(i).

Русский

Элемент g принадлежит f.pi тогда и только тогда, когда для каждого i верно g(i) ∈ f(i).

LaTeX

$$mem_pi {f : Π₀ i, Finset (α i)} {g : DFinsupp fun i => α i} : g ∈ f.pi ↔ ∀ i, g i ∈ f i$$

Lean4

@[simp]
theorem mem_pi {f : Π₀ i, Finset (α i)} {g : Π₀ i, α i} : g ∈ f.pi ↔ ∀ i, g i ∈ f i :=
  mem_dfinsupp_iff_of_support_subset <| Subset.refl _

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