adjoin_empty

Mathlib.Algebra.Algebra.NonUnitalSubalgebra

URI: https://scilib.ai/kg/mathlib#NonUnitalAlgebra.adjoin_empty

English

Adjoin of the empty set is the bottom element.

Русский

Adjoin пустого множества равеннию нижнему элементу (ниже нуля).

LaTeX

$$$\operatorname{adjoin}_R(\varnothing) = \bot$$$

Lean4

@[simp]
theorem adjoin_empty : adjoin R (∅ : Set A) = ⊥ :=
  show adjoin R ⊥ = ⊥ by apply GaloisConnection.l_bot; exact NonUnitalAlgebra.gc

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

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

Разделы

Аффилиация

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