iUnion_of_singleton_coe

Mathlib.Data.Set.Lattice

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

English

For any s ⊆ α, the union over i ∈ s of {i} equals s, i.e., ⋃ i : s, ({(i : α)} : Set α) = s.

Русский

Для подмножества s ⊆ α объединение по i ∈ s множеств {i} равно самому s.

LaTeX

$$$$ \\bigcup_{i \\in s} \\{ i \\} = s. $$$$

Lean4

theorem iUnion_of_singleton_coe (s : Set α) : ⋃ i : s, ({(i : α)} : Set α) = s := by simp

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

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

Разделы

Аффилиация

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