adjoin_eq_sInf — Mathlib

English

For any set s, the subalgebra generated by s is the infimum (greatest lower bound) of all subalgebras of A that contain s.

Русский

Для множества s подалгебра, порожденная s, является инфиминумом (наибольшим нижним пределом) всех подалгебр A, содержащих s.

LaTeX

$$$\\operatorname{adjoin}_R(s) = \\inf\\{ p \\mid p \\text{ is a Subalgebra}_R(A) \\text{ and } s \\subseteq p \\}$$$

Lean4

theorem adjoin_eq_sInf : adjoin R s = sInf {p : Subalgebra R A | s ⊆ p} :=
  le_antisymm (le_sInf fun _ h => adjoin_le h) (sInf_le subset_adjoin)

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