biUnion_pair

Mathlib.Data.Set.Lattice

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

English

The union over x ∈ {a,b} of s(x) equals s(a) ∪ s(b).

Русский

Объединение по x ∈ {a,b} множества s(x) равно s(a) ∪ s(b).

LaTeX

$$$\\\\bigcup_{x \\in \\{ a, b \\}} s(x) = s(a) \\cup s(b)$$$

Lean4

theorem biUnion_pair (a b : α) (s : α → Set β) : ⋃ x ∈ ({ a, b } : Set α), s x = s a ∪ s b := by simp

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

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

Разделы

Аффилиация

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