adjoin_mono

Mathlib.Algebra.Algebra.Subalgebra.Lattice

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

English

Let S be a subalgebra with s ⊆ S and S ≤ adjoin R s; then adjoin R s = S.

Русский

Пусть S — подалгебра, s ⊆ S и S ≤ adjoin R s; тогда adjoin R s = S.

LaTeX

$$$S \\le adjoin\\,R\,s \\quad \\text{and} \\quad s \\subseteq S \\Rightarrow adjoin\\,R\,s = S$$$

Lean4

@[gcongr]
theorem adjoin_mono (H : s ⊆ t) : adjoin R s ≤ adjoin R t :=
  Algebra.gc.monotone_l H

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

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

Разделы

Аффилиация

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