star_subset_adjoin

Mathlib.Algebra.Star.Subalgebra

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

← MathLib Explorer

English

The star of a set is contained in the adjoin of that set: star(s) ⊆ adjoin R s.

Русский

Звёздка множества содержится в порождающем adjoin: star(s) ⊆ adjoin R s.

LaTeX

$$$\star s \subseteq \mathrm{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 Algebra.subset_adjoin

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

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

Разделы

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

Аффилиация

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