instUnion

Mathlib.Data.Set.Defs

URI: https://scilib.ai/kg/mathlib#Set.instUnion

English

The collection Set α is equipped with a binary union operation, defined by s ∪ t as the usual union of sets.

Русский

Множество Set α оборудовано бинарной операцией объединения, заданной как обычное объединение множеств.

LaTeX

$$$\forall s,t \in Set\,\alpha:\ s \cup t \in Set\,\alpha$$$

Lean4

instance : Union (Set α) :=
  ⟨Set.union⟩

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

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

Разделы

Аффилиация

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