pair_symm_iff — Mathlib

English

The independence of {[−x, y]} is equivalent to the independence of {[x, y]}.

Русский

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

LaTeX

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

Lean4

theorem pair_symm_iff : LinearIndependent R ![x, y] ↔ LinearIndependent R ![y, x] :=
  by
  suffices ∀ x y : M, LinearIndependent R ![x, y] → LinearIndependent R ![y, x] by tauto
  simp only [LinearIndependent.pair_iff]
  intro x y h s t
  specialize h t s
  rwa [add_comm, and_comm]

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