span_monotone

Mathlib.LinearAlgebra.Span.Defs

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

English

If s ⊆ p and p ≤ span R s, then span R s = p.

Русский

Если s ⊆ p и p ≤ span_R s, то span_R s = p.

LaTeX

$$$ (h_1 : s \subseteq p) (h_2 : p \le \operatorname{span} R s) : \operatorname{span} R s = p. $$$

Lean4

theorem span_monotone : Monotone (span R : Set M → Submodule R M) := fun _ _ => span_mono

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

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

Разделы

Аффилиация

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