subset_adjoin

Mathlib.Algebra.Algebra.Subalgebra.Lattice

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

English

Any subset s of A is contained in the adjoin of s over R, i.e., s ⊆ adjoin_R s.

Русский

Любое множество s ⊆ A содержится в дополнении к s над R, то есть s ⊆ adjoin_R s.

LaTeX

$$$ s \\subseteq \\mathrm{adjoin} \\, R \\, s $$$

Lean4

@[simp, aesop safe 20 (rule_sets := [SetLike])]
theorem subset_adjoin : s ⊆ adjoin R s :=
  Algebra.gc.le_u_l s

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

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

Разделы

Аффилиация

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