star_subset_adjoin

Mathlib.Algebra.Star.NonUnitalSubalgebra

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

← MathLib Explorer

English

The star of s is contained in adjoin R s: star(s) ⊆ adjoin R s.

Русский

Звёздное изображение множества s содержится в adjoin R s.

LaTeX

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

Lean4

@[simp, aesop safe 20 (rule_sets := [SetLike])]
theorem star_subset_adjoin (s : Set A) : star s ⊆ adjoin R s :=
  Set.subset_union_right.trans <| NonUnitalAlgebra.subset_adjoin R

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

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

Разделы

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

Аффилиация

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