linearIndependent_iff_range — Mathlib

English

Let I be a linearly ordered set and C a subset of I → Bool. The ℤ-linear independence of the family GoodProducts.eval C is equivalent to the ℤ-linear independence of the projected family on the range of C, given by p ↦ p.1.

Русский

Пусть I упорядочено линейно, и C ⊆ I → Bool. Тогда ℤ-линейная независимость семейства GoodProducts.eval C эквивалентна ℤ-линейной независимости проекции на диапазон C, заданной отображением p ↦ p.1.

LaTeX

$$$\\mathrm{LinearIndependent}_{\\mathbb{Z}}\\big( \\mathrm{GoodProducts.eval}(C) \\big) \\;\\Longleftrightarrow\\; \\mathrm{LinearIndependent}_{\\mathbb{Z}}\\big( \\lambda p:\\mathrm{range}(C), p_{1} \\big).$$$

Lean4

theorem linearIndependent_iff_range :
    LinearIndependent ℤ (GoodProducts.eval C) ↔ LinearIndependent ℤ (fun (p : range C) ↦ p.1) :=
  by
  rw [← @Set.rangeFactorization_eq _ _ (GoodProducts.eval C), ← equiv_toFun_eq_eval C]
  exact linearIndependent_equiv (equiv_range C)

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