subset_adjoin

Mathlib.Algebra.Star.NonUnitalSubalgebra

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

← MathLib Explorer

English

Any set s is contained in its adjoin: 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 :=
  Set.subset_union_left.trans <| NonUnitalAlgebra.subset_adjoin R

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

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

Разделы

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

Аффилиация

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