union_univ

Mathlib.Data.Set.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem union_univ (s : Set α) : s ∪ univ = univ :=
  sup_top_eq _

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

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

Разделы

Аффилиация

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