image_span_subset_span

Mathlib.LinearAlgebra.Span.Basic

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

← MathLib Explorer

English

For a semilinear map f, s ⊆ M, the image of span f(s) sits inside span of f(s).

Русский

Образ спана через f множества s содержится в спане образа s.

LaTeX

$$$ f''\operatorname{span}(s) \subseteq \operatorname{span}(f''s) $$$

Lean4

theorem image_span_subset_span (f : F) (s : Set M) : f '' span R s ⊆ span R₂ (f '' s) :=
  (image_span_subset f s _).2 fun x hx ↦ subset_span ⟨x, hx, rfl⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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