eq_of_pair — Mathlib

English

If two vectors x and y form a linearly independent pair, then an equality s x + t y = s' x + t' y implies s=s' and t=t'.

Русский

Если два вектора x,y образуют линейно независимую пару, то равенство s x + t y = s' x + t' y означает s = s' и t = t'.

LaTeX

$$$$\\text{If } \\operatorname{LinearIndependent}_R(\\,[x,y] \\!) \\text{ then } s x + t y = s' x + t' y \\Rightarrow s = s' \\land t = t'.$$$$

Lean4

theorem eq_of_pair {x y : M} (h : LinearIndependent R ![x, y]) {s t s' t' : R} (h' : s • x + t • y = s' • x + t' • y) :
    s = s' ∧ t = t' :=
  pair_iffₛ.mp h _ _ _ _ h'

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