adjoin_singleton_zero

Mathlib.Algebra.Algebra.Subalgebra.Lattice

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

English

The algebra generated by {0} equals the bottom subalgebra.

Русский

Порождение множества {0} даёт дно.

LaTeX

$$$$\\operatorname{adjoin}_R\\{0\\} = \\bot$$$$

Lean4

@[simp]
theorem adjoin_singleton_zero : adjoin R ({0} : Set A) = ⊥ :=
  mod_cast adjoin_singleton_natCast R A 0

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

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

Разделы

Аффилиация

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