mem_pi — Mathlib

English

An element x of the product ∏_i S_i lies in π(s,t) exactly when each coordinate x_i lies in t_i for indices i in s.

Русский

Элемент x из произведения ∏_i S_i принадлежит π(s,t) тогда и только тогда, когда для каждого i из s координата x_i принадлежит t_i.

LaTeX

$$$x\in \pi(s,t) \iff \forall i\in s,\ x_i\in t_i$$$

Lean4

@[simp]
theorem mem_pi : x ∈ pi s t ↔ ∀ i ∈ s, x i ∈ t i :=
  .rfl

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