adjoin_toSubmodule_le — Mathlib

English

The span of a set s is contained in the submodule corresponding to adjoin R s.

Русский

Окружение множества s вкладывается в соответствующее подмодуль adjoin R s.

LaTeX

$$$$\\operatorname{span}_R(s) \\le \\operatorname{toSubmodule}(\\operatorname{adjoin}_R s)$$$$

Lean4

theorem adjoin_toSubmodule_le {s : Set A} {t : Submodule R A} :
    Subalgebra.toSubmodule (adjoin R s) ≤ t ↔ ↑(Submonoid.closure s) ⊆ (t : Set A) := by rw [adjoin_eq_span, span_le]

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