exists_linearIndepOn_id_extension

English

Let hs express that the identity embedding is LI on s, and s ⊆ t. Then there exists b ⊆ t with s ⊆ b, t ⊆ span_K b, and b is LI with respect to the identity embedding.

Русский

Пусть hs выражает, что отображение тождественно LI на s, и s ⊆ t. Тогда существует b ⊆ t, такое что s ⊆ b, t ⊆ span_K b, и b линейно независимо относительно тождественной вложенности.

LaTeX

$$$$\exists b \subseteq t,\ s \subseteq b \land t \subseteq \operatorname{span}_K b \land \ LinearIndepOn\ K\ id\ b.$$$$

Lean4

theorem exists_linearIndepOn_id_extension (hs : LinearIndepOn K id s) (hst : s ⊆ t) :
    ∃ b ⊆ t, s ⊆ b ∧ t ⊆ span K b ∧ LinearIndepOn K id b := by convert exists_linearIndepOn_extension hs hst <;> simp

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