English
If u is a sub-ambient where the inclusion is LI, and s,t ⊆ u with span s ≤ span t, then s ⊆ t.
Русский
Если u задаёт линейно независимый настраиваемый подмножество включения, и s,t ⊆ u с span s ≤ span t, тогда s ⊆ t.
LaTeX
$$$\\text{LinearIndepOn } R\\ id\\ u \\rightarrow s\\subseteq u \\rightarrow t\\subseteq u \\rightarrow \\operatorname{span}_R s \\le \\operatorname{span}_R t \\rightarrow s\\subseteq t$$$
Lean4
theorem le_of_span_le_span [Nontrivial R] {s t u : Set M} (hl : LinearIndepOn R id u) (hsu : s ⊆ u) (htu : t ⊆ u)
(hst : span R s ≤ span R t) : s ⊆ t :=
by
have :=
eq_of_linearIndepOn_id_of_span_subtype (hl.mono (Set.union_subset hsu htu)) Set.subset_union_right
(Set.union_subset (Set.Subset.trans subset_span hst) subset_span)
rw [← this]; apply Set.subset_union_left
