English
If the restriction of the identity map to a is linearly independent on s, and t ⊆ s, and s ⊆ span R t, then s = t.
Русский
Если ограничение тождества к s линейно независимо на s и t ⊆ s, а s ⊆ span R t, то s = t.
LaTeX
$$$\\text{LinearIndepOn } R\\ id\\ s \\rightarrow t\\subseteq s \\rightarrow s\\subseteq \\operatorname{span}_R t \\rightarrow s=t$$$
Lean4
theorem eq_of_linearIndepOn_id_of_span_subtype [Nontrivial R] {s t : Set M} (hs : LinearIndepOn R id s) (h : t ⊆ s)
(hst : s ⊆ span R t) : s = t :=
by
let f : t ↪ s := ⟨fun x => ⟨x.1, h x.2⟩, fun a b hab => Subtype.coe_injective (Subtype.mk.inj hab)⟩
have h_surj : Surjective f := by
apply surjective_of_linearIndependent_of_span hs f _
convert hst <;> simp [f, comp_def]
change s = t
apply Subset.antisymm _ h
intro x hx
rcases h_surj ⟨x, hx⟩ with ⟨y, hy⟩
convert y.mem
rw [← Subtype.mk.inj hy]
