span_mono

Mathlib.RingTheory.Ideal.Span

URI: https://scilib.ai/kg/mathlib#Ideal.span_mono

English

If s ⊆ t, then span(s) ≤ span(t).

Русский

Если s ⊆ t, то span(s) ≤ span(t).

LaTeX

$$$s \\subseteq t \\Rightarrow \\operatorname{span}(s) \\le \\operatorname{span}(t)$$$

Lean4

@[gcongr]
theorem span_mono {s t : Set α} : s ⊆ t → span s ≤ span t :=
  Submodule.span_mono

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

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

Разделы

Аффилиация

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