add_eq_sup

Mathlib.Algebra.Order.Kleene

URI: https://scilib.ai/kg/mathlib#add_eq_sup

English

In an IdemSemiring, addition coincides with the join in the induced order: a + b = a ⊔ b.

Русский

В IdemSemiring сложение совпадает с объединением в порожденном порядке: a + b = a ⊔ b.

LaTeX

$$$ a + b = a \sqcup b $$$

Lean4

theorem add_eq_sup (a b : α) : a + b = a ⊔ b :=
  IdemSemiring.add_eq_sup _ _

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

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

Разделы

Аффилиация

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