toSet_sUnion

Mathlib.SetTheory.ZFC.Basic

URI: https://scilib.ai/kg/mathlib#ZFSet.toSet_sUnion

English

The toSet of a union equals the union of the toSet image of elements.

Русский

toSet объединения равен объединению изображений toSet элементов.

LaTeX

$$$ (\bigcup x).toSet = \bigcup (\mathrm{toSet}'' x.toSet) $$$

Lean4

@[simp]
theorem toSet_sUnion (x : ZFSet.{u}) : (⋃₀ x).toSet = ⋃₀ (toSet '' x.toSet) :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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