mem_pi — Mathlib

English

Membership in pi I H is equivalent to pointwise membership: p ∈ pi I H iff ∀ i, i ∈ I → p(i) ∈ H(i).

Русский

Членство в pi I H эквивалентно покоординатному членству: p ∈ pi I H тогда и только если ∀ i, i ∈ I → p(i) ∈ H(i).

LaTeX

$$$ p \in \mathrm{pi} I H \iff \forall i, i \in I \to p(i) \in H(i) $$$

Lean4

@[to_additive]
theorem mem_pi (I : Set η) {H : ∀ i, Subgroup (f i)} {p : ∀ i, f i} : p ∈ pi I H ↔ ∀ i : η, i ∈ I → p i ∈ H i :=
  Iff.rfl

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