biUnion_of_singleton

Mathlib.Data.Set.Lattice

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

English

The union over x ∈ s of {x} equals s.

Русский

Объединение по x ∈ s множества {x} равно s.

LaTeX

$$$\\\\bigcup_{x \\in s} \\{x\\} = s$$$

Lean4

@[simp]
theorem biUnion_of_singleton (s : Set α) : ⋃ x ∈ s, { x } = s :=
  ext <| by simp

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

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

Разделы

Аффилиация

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