linearIndepOn_id' — Mathlib

English

A version of independence on a set s with a shortened or extended domain remains equivalent under suitable mapping to subdomains.

Русский

Версия независимости на множестве s сохраняется при подходящем отображении на подсхему.

LaTeX

$$$\\\\mathrm{LinearIndepOn}_R v s \\\\iff \\\\exists f,g : \\iota \\to R, \\\\sum_{i \\in s} f(i) v_i = \\sum_{i \\in s} g(i) v_i \\\\land \\\\exists i \\in s, f(i) \\neq g(i).$$$

Lean4

/-- A version of `LinearIndependent.linearIndepOn_id` with the set range equality as a hypothesis.
-/
theorem linearIndepOn_id' (hv : LinearIndependent R v) {t : Set M} (ht : Set.range v = t) : LinearIndepOn R id t :=
  ht ▸ hv.linearIndepOn_id

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