exists_finite_card_le_of_finite_of_linearIndependent_of_span

English

For a linear independent On on s and s ⊆ span K t (t finite), there exists t' with properties ensuring same span and containment similar to the finite-span lemma above.

Русский

Для линейной независимости на s и s ⊆ span K t (t конечно), существует t' со свойствами, сохраняющими тот же порождающий спан и включение как в предыдущем лемме.

LaTeX

$$$$\exists t' : Finset V, ↑t' ⊆ s ∪ ↑t \land s ⊆ ↑t' \land t'.card = t.card.$$$$

Lean4

theorem exists_finite_card_le_of_finite_of_linearIndependent_of_span {s t : Set V} (ht : t.Finite)
    (hs : LinearIndepOn K id s) (hst : s ⊆ span K t) : ∃ h : s.Finite, h.toFinset.card ≤ ht.toFinset.card :=
  have : s ⊆ (span K ↑ht.toFinset : Submodule K V) := by simpa
  let ⟨u, _hust, hsu, Eq⟩ := exists_of_linearIndepOn_of_finite_span hs this
  have : s.Finite := u.finite_toSet.subset hsu
  ⟨this, by rw [← Eq]; exact Finset.card_le_card <| Finset.coe_subset.mp <| by simp [hsu]⟩

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