exists_linearIndependent — Mathlib

English

There exists a subset b ⊆ t such that span_K{v i : i ∈ b} equals span_K{v i : i ∈ t} and the family {v i : i ∈ b} is linearly independent.

Русский

Существует подмножество b ⊆ t такое, что span_K{v i : i ∈ b} приближает span_K{v i : i ∈ t} и множество {v i : i ∈ b} линейно независимо.

LaTeX

$$$$\exists b \subseteq t,\ span_K\{v_i : i\in b\} = span_K\{v_i : i\in t\} \land \{v_i : i\in b\} \text{ линейно независимо}.$$$$

Lean4

theorem exists_linearIndependent : ∃ b ⊆ t, span K b = span K t ∧ LinearIndependent K ((↑) : b → V) :=
  by
  obtain ⟨b, hb₁, -, hb₂, hb₃⟩ := exists_linearIndepOn_id_extension (linearIndependent_empty K V) (Set.empty_subset t)
  exact ⟨b, hb₁, (span_eq_of_le _ hb₂ (Submodule.span_mono hb₁)).symm, hb₃⟩

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