star_preimage

Mathlib.Algebra.Star.Pointwise

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

English

The preimage of a set under star equals its star: Star.star ⁻¹' s = s⋆.

Русский

Прообраз множества под действием звезды равен его звёздному образу: Star.star ⁻¹' s = s⋆.

LaTeX

$$$\\mathrm{Star}.star^{-1}(s) = s^{\\star}.$$$

Lean4

@[simp]
theorem star_preimage [Star α] : Star.star ⁻¹' s = s⋆ :=
  rfl

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

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

Разделы

Аффилиация

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