mem_pi — Mathlib

English

Let I be a set of indices and S_i a submonoid for each i. For p: ∀ i, M_i, membership of p in Submonoid.pi I S is equivalent to saying p(i) ∈ S_i for every i with i ∈ I.

Русский

Пусть I — множество индексов и для каждого i задан подмножество-подмонoид S_i. Тогда p ∈ Submonoid.pi I S эквивалентно тому, что p(i) ∈ S_i для каждого i, если i ∈ I.

LaTeX

$$$ p \in Submonoid.pi I S \iff ∀ i, i ∈ I \rightarrow p i ∈ S i $$$

Lean4

@[to_additive]
theorem mem_pi (I : Set ι) {S : ∀ i, Submonoid (M i)} {p : ∀ i, M i} : p ∈ Submonoid.pi I S ↔ ∀ i, i ∈ I → p i ∈ S i :=
  Iff.rfl

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