mem_span_of_mem

Mathlib.LinearAlgebra.Span.Defs

URI: https://scilib.ai/kg/mathlib#Submodule.mem_span_of_mem

English

If x ∈ s, then x ∈ span R s.

Русский

Если x ∈ s, то x ∈ span_R s.

LaTeX

$$$ x \in s \Rightarrow x \in \operatorname{span} R s. $$$

Lean4

@[aesop 80% (rule_sets := [SetLike])]
theorem mem_span_of_mem {s : Set M} {x : M} (hx : x ∈ s) : x ∈ span R s :=
  subset_span hx

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru