some_union_some

Mathlib.Data.Part

URI: https://scilib.ai/kg/mathlib#Part.some_union_some

English

some a ∪ some b equals some (a ∪ b).

Русский

some a ∪ some b равно some (a ∪ b).

LaTeX

$$$$ \mathrm{some}(a) \cup \mathrm{some}(b) = \mathrm{some}(a \cup b). $$$$

Lean4

theorem some_union_some [Union α] (a b : α) : some a ∪ some b = some (a ∪ b) := by simp [union_def]

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

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

Разделы

Аффилиация

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