adjoin_eq

Mathlib.Algebra.Star.NonUnitalSubalgebra

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

← MathLib Explorer

English

adjoin R s ≤ S if and only if s ⊆ S.

Русский

adjoin_R(s) ≤ S тогда и только тогда, когда s ⊆ S.

LaTeX

$$$$ \\\\operatorname{adjoin}_R(s) \\\\le S \\\\iff s \\\\subseteq S $$$$

Lean4

@[simp]
theorem adjoin_eq (s : NonUnitalStarSubalgebra R A) : adjoin R (s : Set A) = s :=
  le_antisymm (adjoin_le le_rfl) (subset_adjoin R (s : Set A))

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

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

Разделы

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

Аффилиация

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