biUnion_empty

Mathlib.Data.Set.Lattice

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

English

For any u: α → Set β, the union over x ∈ ∅ of u(x) equals ∅.

Русский

Для любой u: α → Set β объединение по x ∈ ∅ u(x) равно пустому множеству.

LaTeX

$$$\\\\bigcup_{x \\in \\varnothing} u(x) = \\varnothing$$$

Lean4

theorem biUnion_empty (s : α → Set β) : ⋃ x ∈ (∅ : Set α), s x = ∅ :=
  iSup_emptyset

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

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

Разделы

Аффилиация

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