mem_pi

Mathlib.LinearAlgebra.Pi

URI: https://scilib.ai/kg/mathlib#Submodule.mem_pi

English

An element x lies in pi(I, p) exactly when each coordinate x_i lies in p_i for all i ∈ I.

Русский

Элемент x принадлежит π(I, p) тогда и только тогда, когда каждый компонент x_i ∈ p_i при каждом i ∈ I.

LaTeX

$$$$x\\in\\pi(I,p) \\iff \\forall i,\\ i\\in I \\Rightarrow x(i)\\in p(i).$$$$

Lean4

@[simp]
theorem mem_pi : x ∈ pi I p ↔ ∀ i ∈ I, x i ∈ p i :=
  Iff.rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru