linearIndepOn_univ — Mathlib

English

A standard equivalence: independence over the whole index set is equivalent to independence of the mapped family after applying an index-equivalence to the entire domain.

Русский

Стандартное эквивалентность: независимость над всем множеством индексов эквивалентна независимости образованной после применения отображения индексов.

LaTeX

$$$\\\\mathrm{LinearIndepOn}_R v \\\\iff \\\\mathrm{LinearIndependent}_R v \\,\\text{ with } s = \\mathrm{univ}.$$$

Lean4

@[simp]
theorem linearIndepOn_univ : LinearIndepOn R v univ ↔ LinearIndependent R v :=
  linearIndependent_equiv' (Equiv.Set.univ ι) rfl

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