sUnion_pair

Mathlib.Data.Set.Lattice

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

English

Let s and t be subsets of α. The union over the two-element set {s, t} equals s ∪ t: ⋃₀ { s, t } = s ∪ t.

Русский

Пусть s и t — подмножества α. Объединение над двумя элементами {s, t} равно s ∪ t: ⋃₀ { s, t } = s ∪ t.

LaTeX

$$$$ \\bigcup_{U \\in \\{s, t\\}} U = s \\cup t. $$$$

Lean4

theorem sUnion_pair (s t : Set α) : ⋃₀ { s, t } = s ∪ t :=
  sSup_pair

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

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

Разделы

Аффилиация

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