nonempty_linearIndependent_set — Mathlib

English

There exists a subset of M which is linearly independent over R (the empty set provides independence).

Русский

Существует подмножество M, которое линейно независимо над R (пустое множество тоже независимо).

LaTeX

$$$\exists S \subseteq M, \ S \text{ линейно независимо над } R$$$

Lean4

instance nonempty_linearIndependent_set : Nonempty { s : Set M // LinearIndepOn R id s } :=
  ⟨⟨∅, linearIndepOn_empty _ _⟩⟩

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