image_val_iUnion

Mathlib.Data.Set.Subset

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

English

The image of the indexed union equals the indexed union of images.

Русский

Образ iUnion равен iUnion образов.

LaTeX

$$$\\operatorname{image}(\\operatorname{val})(\\bigcup_i t_i) = \\bigcup_i (\\operatorname{image}(\\operatorname{val}) (t_i))$$$

Lean4

@[simp]
theorem image_val_iUnion : ↑(⋃ i, t i) = ⋃ i, (t i : Set α) :=
  image_iUnion

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

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

Разделы

Аффилиация

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