adjoin_eq_of_le

Mathlib.Algebra.Algebra.Subalgebra.Lattice

URI: https://scilib.ai/kg/mathlib#Algebra.adjoin_eq_of_le

English

For a Subalgebra S, adjoin R ↑S equals S.

Русский

Для подалгебры S выполняется adjoin R ↑S = S.

LaTeX

$$$\\operatorname{adjoin}^R(\\operatorname{SetLike}.coe S) = S$$$

Lean4

theorem adjoin_eq_of_le (S : Subalgebra R A) (h₁ : s ⊆ S) (h₂ : S ≤ adjoin R s) : adjoin R s = S :=
  le_antisymm (adjoin_le h₁) h₂

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

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

Разделы

Аффилиация

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