adjoin_le — Mathlib

English

The star-subalgebra generated by s has its underlying submodule equal to the span of the monoid closure of s ∪ s*, i.e., adjoin R s has the same span as span of closure of s ∪ s*.

Русский

Звёздная подалгебра, порождаемая s, имеет подмодуль-образ, равный линейному сепаратору замкнутого множества монойды s ∪ s^*, т.е. adjoin R s имеет тот же span, что и span(closure(s ∪ s^*)).

LaTeX

$$$\mathrm{adjoin}(R,s)^{\,toSubalgebra}\; =\; \mathrm{span}\,R\big( \mathrm{Submonoid.closure}(s \cup s^{*})\big).$$$

Lean4

theorem adjoin_le {S : StarSubalgebra R A} {s : Set A} (hs : s ⊆ S) : adjoin R s ≤ S :=
  StarAlgebra.gc.l_le hs

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