iInter_star

Mathlib.Algebra.Star.Pointwise

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

English

The star commutes with indexed intersections: (⋂ i, s_i)⋆ = ⋂ i, (s_i)⋆.

Русский

Звезда commuting с пересечением по индексу: (⋂ i, s_i)⋆ = ⋂ i, (s_i)⋆.

LaTeX

$$$\\big(\\big\\cap_i s_i\\big)^{\\star} = \\bigcap_i s_i^{\\star}.$$$

Lean4

@[simp]
theorem iInter_star {ι : Sort*} [Star α] (s : ι → Set α) : (⋂ i, s i)⋆ = ⋂ i, (s i)⋆ :=
  preimage_iInter

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

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

Разделы

Аффилиация

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