adjoin_singleton_le — Mathlib

English

Let S be a subalgebra of A over R. If a ∈ S, then the smallest subalgebra containing a lies inside S; i.e., adjoin_R{a} ⊆ S.

Русский

Пусть S является подалгеброй A над R. Пусть a ∈ S. Тогда порождающая подалгебра, порожденная элементом a, содержится в S: adjoin_R{a} ⊆ S.

LaTeX

$$$\operatorname{adjoin}_R\{a\} \le S$$$

Lean4

theorem adjoin_singleton_le {S : Subalgebra R A} {a : A} (H : a ∈ S) : adjoin R { a } ≤ S :=
  adjoin_le (Set.singleton_subset_iff.mpr H)

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