span_le_adjoin — Mathlib

English

The inclusion adjoin R s ≤ t (as a submodule) holds if and only if the underlying set of the submonoid closure of s is contained in t.

Русский

Предел включения adjoin_R s ≤ t эквивалентен тому, что порождение подмодуля через замыкание множества s лежит в t.

LaTeX

$$$$\\operatorname{adjoin}_R s \\le t \\quad \\Leftrightarrow \\; \\uparrow(\\operatorname{Submonoid.closure} s) \\subseteq t$$$$

Lean4

theorem span_le_adjoin (s : Set A) : span R s ≤ Subalgebra.toSubmodule (adjoin R s) :=
  span_le.mpr subset_adjoin

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