adjoin_eq

Mathlib.Algebra.Star.Subalgebra

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

English

A simplification of adjoin_le_iff: adjoin R s ≤ S iff s ⊆ S, expressed via the simplified Galois connection.

Русский

Упрощённое выражение adjoin_le_iff: adjoin R s ≤ S ⇔ s ⊆ S, через Гало-соединение.

LaTeX

$$$\mathrm{adjoin}(R,s) \le S \iff s \subseteq S$$$

Lean4

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

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

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

Разделы

Аффилиация

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