iUnion_inv

Mathlib.Algebra.Group.Pointwise.Set.Lattice

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

English

The inverse of a union distributes over the union: (⋃ i, s_i)^{-1} = ⋃ i, (s_i)^{-1}.

Русский

Обратное к объединению распределяется по объединениям: (⋃ i, s_i)^{-1} = ⋃ i, s_i^{-1}.

LaTeX

$$$\\left(\\bigcup_i s_i\\right)^{-1} = \\bigcup_i (s_i)^{-1}$$$

Lean4

@[to_additive (attr := simp)]
theorem iUnion_inv (s : ι → Set α) : (⋃ i, s i)⁻¹ = ⋃ i, (s i)⁻¹ :=
  preimage_iUnion

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

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

Разделы

Аффилиация

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