mem_pi — Mathlib

English

In the pi-construction, membership is coordinatewise: x ∈ pi s L iff for all i, i ∈ s implies x(i) ∈ L(i).

Русский

В конструировании pi членство определяется по координатам: x ∈ pi s L ⇔ ∀ i, i ∈ s → x(i) ∈ L(i).

LaTeX

$$x \\in \\pi s L \\iff \\forall i, i \\in s \\to x(i) \\in L(i)$$

Lean4

@[simp]
theorem mem_pi {s : Set κ} {L : ∀ i, Sublattice (π i)} {x : ∀ i, π i} : x ∈ pi s L ↔ ∀ i, i ∈ s → x i ∈ L i :=
  Iff.rfl

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