mem_span_singleton_trans

Mathlib.LinearAlgebra.Span.Defs

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

← MathLib Explorer

English

If x ∈ R ∙ y and y ∈ R ∙ z, then x ∈ R ∙ z.

Русский

Если x ∈ R ∙ y и y ∈ R ∙ z, то x ∈ R ∙ z.

LaTeX

$$$$ x \\in R \\cdot y \\Rightarrow y \\in R \\cdot z \\Rightarrow x \\in R \\cdot z. $$$$

Lean4

theorem mem_span_singleton_trans {x y z : M} (hxy : x ∈ R ∙ y) (hyz : y ∈ R ∙ z) : x ∈ R ∙ z :=
  by
  rw [← SetLike.mem_coe, ← singleton_subset_iff] at *
  exact Submodule.subset_span_trans hxy hyz

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

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

Разделы

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

Аффилиация

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