English
If s ⊆ span t and t ⊆ span s, then span s = span t.
Русский
Если s ⊆ span t и t ⊆ span s, то span s = span t.
LaTeX
$$$ hs : s \subseteq \operatorname{span} R t \rightarrow ht : t \subseteq \operatorname{span} R s \rightarrow \operatorname{span} R s = \operatorname{span} R t. $$$
Lean4
/-- A version of `Submodule.span_eq` for subobjects closed under addition and scalar multiplication
and containing zero. In general, this should not be used directly, but can be used to quickly
generate proofs for specific types of subobjects. -/
theorem coe_span_eq_self [SetLike S M] [AddSubmonoidClass S M] [SMulMemClass S R M] (s : S) :
(span R (s : Set M) : Set M) = s := by
refine le_antisymm ?_ subset_span
let s' : Submodule R M :=
{ carrier := s
add_mem' := add_mem
zero_mem' := zero_mem _
smul_mem' := SMulMemClass.smul_mem }
exact span_le (p := s') |>.mpr le_rfl
