star_univ

Mathlib.Algebra.Star.Pointwise

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

English

The star of the universal set is universal: univ⋆ = univ.

Русский

Звезда вселенной равна вселенной: univ⋆ = univ.

LaTeX

$$$(\\mathrm{univ})^{\\star} = \\mathrm{univ}.$$$

Lean4

@[simp]
theorem star_univ [Star α] : (univ : Set α)⋆ = univ :=
  rfl

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

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

Разделы

Аффилиация

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