small_adjoin — Mathlib

English

If R is small, then the adjoin of any set s in S is small as a subalgebra of S.

Русский

Если R мал, то порождение множества s в S образует малый подалгебраический элемент.

LaTeX

$$$Small(R) \Rightarrow Small(\operatorname{adjoin}_R s : Subalgebra R S)$$$

Lean4

instance small_adjoin [Small.{u} R] {s : Set S} [Small.{u} s] : Small.{u} (adjoin R s : Subalgebra R S) :=
  by
  rw [Algebra.adjoin_eq_range]
  apply small_range

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