sups_singleton

Mathlib.Data.Finset.Sups

URI: https://scilib.ai/kg/mathlib#Finset.sups_singleton

English

The supersets of two singletons {a} and {b} merge to the singleton {a ⊔ b}.

Русский

Объединение двух одиночных множеств {a} и {b} даёт множество {a ⊔ b}.

LaTeX

$$$\{a\} \oplus \{b\} = \{a \sqcup b\}$$$

Lean4

@[simp]
theorem sups_singleton : s ⊻ { b } = s.image (· ⊔ b) :=
  image₂_singleton_right

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

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

Разделы

Аффилиация

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