sup_eq_union

Mathlib.Data.Set.Basic

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

English

The join operation on Set α coincides with set union: sup = union.

Русский

Операция согласования верхних элементов (join) в Set α совпадает с объединением: sup = ∪.

LaTeX

$$$\\text{(sup)} = (\\cup)$$$

Lean4

@[simp]
theorem sup_eq_union : ((· ⊔ ·) : Set α → Set α → Set α) = (· ∪ ·) :=
  rfl

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

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

Разделы

Аффилиация

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