univ_union

Mathlib.Data.Set.Basic

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

English

Let S be any set. Then univ ∪ S = univ.

Русский

Пусть S — произвольное множество. Тогда вселенная ∪ S = вселенная.

LaTeX

$$$U \cup S = U$$$

Lean4

@[simp]
theorem univ_union (s : Set α) : univ ∪ s = univ :=
  top_sup_eq _

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

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

Разделы

Аффилиация

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