toSet_sUnion

Mathlib.SetTheory.ZFC.PSet

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

English

The toSet of the sUnion of x equals the sUnion of the toSet image of x.

Русский

toSet от объединения ⋃₀ x равно объединению toSet изображения x.

LaTeX

$$$$ (\bigcup_{0} x).toSet = \bigcup_{0} (toSet '' x.toSet) $$$$

Lean4

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

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

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

Разделы

Аффилиация

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