union_assoc

Mathlib.Data.Finmap

URI: https://scilib.ai/kg/mathlib#Finmap.union_assoc

← MathLib Explorer

English

Union is associative: s1 ∪ (s2 ∪ s3) = (s1 ∪ s2) ∪ s3.

Русский

Объединение ассоциативно: s1 ∪ (s2 ∪ s3) = (s1 ∪ s2) ∪ s3.

LaTeX

$$$ s_1 \cup s_2 \cup s_3 = s_1 \cup (s_2 \cup s_3) $$$

Lean4

theorem union_assoc {s₁ s₂ s₃ : Finmap β} : s₁ ∪ s₂ ∪ s₃ = s₁ ∪ (s₂ ∪ s₃) :=
  induction_on₃ s₁ s₂ s₃ fun s₁ s₂ s₃ => by simp only [AList.toFinmap_eq, union_toFinmap, AList.union_assoc]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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