linearIndepOn_id_pair — Mathlib

English

For x,y ∈ V, if x ≠ 0 and no scalar multiple of x equals y, then {x,y} is linearly independent with respect to id.

Русский

Для векторов x и y в V, если x ≠ 0 и нет скаляра a такой, что a x = y, то семейство {x,y} линейно независимо относительно id.

LaTeX

$$$x \\neq 0 \\Rightarrow \\bigl( \\forall a \\in K,\ a \\cdot x \\neq y \\bigr) \\Rightarrow \\text{LinearIndepOn}_K(\\mathrm{id},\\{x,y\\})$$$

Lean4

theorem linearIndepOn_id_pair {x y : V} (hx : x ≠ 0) (hy : ∀ a : K, a • x ≠ y) : LinearIndepOn K id { x, y } :=
  pair_comm y x ▸ (LinearIndepOn.id_singleton K hx).id_insert (x := y) <| mt mem_span_singleton.1 <| not_exists.2 hy

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