sUnion_singleton

Mathlib.SetTheory.ZFC.Basic

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

English

The union of a singleton {x} equals x.

Русский

Объединение одиночного множества {x} равно x.

LaTeX

$$$ \bigcup_0 \{ x \} = x $$$

Lean4

@[simp]
theorem sUnion_singleton {x : ZFSet.{u}} : ⋃₀ ({ x } : ZFSet) = x :=
  ext fun y => by simp_rw [mem_sUnion, mem_singleton, exists_eq_left]

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

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

Разделы

Аффилиация

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