pair_iff — Mathlib

English

Independence of {x, y} is equivalent to independence of {y, x}.

Русский

Независимость множества {x, y} эквивалентна независимости множества {y, x}.

LaTeX

$$$\\mathrm{LinearIndependent}_R(\\![x,y\\]) \\iff \\mathrm{LinearIndependent}_R(\\![y,x\\])$$$

Lean4

/-- Also see `LinearIndependent.pair_iff'` for a simpler version over fields. -/
theorem pair_iff : LinearIndependent R ![x, y] ↔ ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0 :=
  by
  rw [← linearIndepOn_univ, ← Finset.coe_univ, show @Finset.univ (Fin 2) _ = {0, 1} from rfl, Finset.coe_insert,
    Finset.coe_singleton, LinearIndepOn.pair_iff _ (by trivial)]
  simp

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