iUnion_star

Mathlib.Algebra.Star.Pointwise

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

English

Star distributes over indexed unions: (⋃ i, s_i)⋆ = ⋃ i, (s_i)⋆.

Русский

Звезда распределяется по объединениям индексированных множества: (⋃ i, s_i)⋆ = ⋃ i, (s_i)⋆.

LaTeX

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

Lean4

@[simp]
theorem iUnion_star {ι : Sort*} [Star α] (s : ι → Set α) : (⋃ i, s i)⋆ = ⋃ i, (s i)⋆ :=
  preimage_iUnion

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

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

Разделы

Аффилиация

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