linearIndependent_subtype_iff — Mathlib

English

Linear independence of a family of subtypes is equivalent to LinearIndepOn with identity on the index set.

Русский

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

LaTeX

$$$\\operatorname{LinearIndependent}(R,\\operatorname{Subtype.val}:s\\to M) \\iff \\operatorname{LinearIndepOn}(R,\\operatorname{id},s)$$$

Lean4

theorem linearIndependent_subtype_iff {s : Set M} : LinearIndependent R (Subtype.val : s → M) ↔ LinearIndepOn R id s :=
  Iff.rfl

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