add_def

Mathlib.Data.Set.Semiring

URI: https://scilib.ai/kg/mathlib#SetSemiring.add_def

English

Addition in SetSemiring corresponds to union; s + t equals the up of the union of s.down and t.down.

Русский

Сложение в SetSemiring соответствует объединению: s + t = (s.down ∪ t.down).up.

LaTeX

$$s + t = (s.down \cup t.down).up$$

Lean4

theorem add_def (s t : SetSemiring α) : s + t = (s.down ∪ t.down).up :=
  rfl

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

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

Разделы

Аффилиация

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