subset_span

Mathlib.RingTheory.TwoSidedIdeal.Operations

URI: https://scilib.ai/kg/mathlib#TwoSidedIdeal.subset_span

← MathLib Explorer

English

Every element of a set s is contained in span(s).

Русский

Каждый элемент множества s содержится в span(s).

LaTeX

$$s ⊆ (span s)$$

Lean4

theorem subset_span {s : Set R} : s ⊆ (span s : Set R) :=
  by
  intro x hx
  rw [SetLike.mem_coe, mem_iff]
  exact RingConGen.Rel.of _ _ (by simpa using hx)

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

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

Разделы

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

Аффилиация

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