mem_span_pair — Mathlib

English

Let x, y, z ∈ M. An element z lies in the span of {x, y} if and only if there exist scalars a, b ∈ R such that z = a x + b y.

Русский

Пусть x, y, z ∈ M. Элемент z принадлежит линейной оболочке множества {x, y} тогда и только тогда существуют скаляры a, b ∈ R такие, что z = a x + b y.

LaTeX

$$$ z \in \operatorname{span}_R\left(\{x, y\}\right) \Longleftrightarrow \exists a,b \in R, a \cdot x + b \cdot y = z $$$

Lean4

theorem mem_span_pair {x y z : M} : z ∈ span R ({ x, y } : Set M) ↔ ∃ a b : R, a • x + b • y = z := by
  simp_rw [mem_span_insert, mem_span_singleton, exists_exists_eq_and, eq_comm]

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