iUnion_nonempty_self

Mathlib.Data.Set.Lattice

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

English

If s is a nonempty subset of α, then the union over x in s of s equals s.

Русский

Если s непусто как подмножество α, то объединение по x в s множества s равно s.

LaTeX

$$$s \\neq \\varnothing \\Rightarrow \\bigcup_{x \\in s} s = s$$$

Lean4

@[simp]
theorem iUnion_nonempty_self (s : Set α) : ⋃ _ : s.Nonempty, s = s := by rw [iUnion_nonempty_index, biUnion_self]

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

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

Разделы

Аффилиация

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