star

Mathlib.Algebra.Star.Pointwise

URI: https://scilib.ai/kg/mathlib#Set.Finite.star

English

If s is finite, then s⋆ is finite.

Русский

Если s конечное, то s⋆ конечное.

LaTeX

$$$s\\text{ finite} \\Rightarrow s^{\\star}\\ \\text{finite}$.$$

Lean4

theorem star [InvolutiveStar α] {s : Set α} (hs : s.Finite) : s⋆.Finite :=
  hs.preimage star_injective.injOn

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

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

Разделы

Аффилиация

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