mem_span_pair — Mathlib

English

An element z lies in the span of {x,y} if and only if z = a x + b y for some a,b.

Русский

Элемент z принадлежит порождению {x,y} тогда и только тогда, когда z = a x + b y для некоторых a,b.

LaTeX

$$$$ z \in \operatorname{span} (\{ x, y \} : Set \alpha) \iff \exists a,b,\ a x + b y = z $$$$

Lean4

theorem mem_span_pair {x y z : α} : z ∈ span ({ x, y } : Set α) ↔ ∃ a b, a * x + b * y = z :=
  Submodule.mem_span_pair

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