subset_adjoin

Mathlib.Algebra.Algebra.NonUnitalSubalgebra

URI: https://scilib.ai/kg/mathlib#NonUnitalAlgebra.subset_adjoin

← MathLib Explorer

English

Every element of s is contained in the adjoin of s; i.e., s ⊆ adjoin R s.

Русский

Каждый элемент множества s принадлежит adjoin R s.

LaTeX

$$$s \subseteq \operatorname{adjoin}_R(s)$$$

Lean4

@[simp, aesop safe 20 (rule_sets := [SetLike])]
theorem subset_adjoin {s : Set A} : s ⊆ adjoin R s :=
  NonUnitalSubsemiring.subset_closure.trans Submodule.subset_span

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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