union_insert

Mathlib.Data.Set.Insert

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

English

Insertion distributes over union: insert a (s ∪ t) equals insert a s union insert a t.

Русский

Вставка распределяется над объединением: insert a (s ∪ t) = insert a s ∪ insert a t.

LaTeX

$$$\operatorname{insert} a (s \cup t) = \operatorname{insert} a s \cup \operatorname{insert} a t$$$

Lean4

@[simp]
theorem union_insert : s ∪ insert a t = insert a (s ∪ t) := by grind

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

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

Разделы

Аффилиация

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