star_empty

Mathlib.Algebra.Star.Pointwise

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

English

The star of the empty set is empty: ∅⋆ = ∅.

Русский

Звезда пустого множества равна пустому множеству: ∅⋆ = ∅.

LaTeX

$$$\\emptyset^{\\star} = \\emptyset.$$$

Lean4

@[simp]
theorem star_empty [Star α] : (∅ : Set α)⋆ = ∅ :=
  rfl

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

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

Разделы

Аффилиация

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