Union_is_Associative

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

associativitydirect-proofsproofwikiset-unionunion-is-associative

Set union is associative: A ∪ (B ∪ C) = (A ∪ B) ∪ C

Preamble

import Mathlib.Data.Set.Basic
import Mathlib.Tactic

Formal statement

theorem Union_is_Associative {α : Type*} (A B C : Set α) : A ∪ (B ∪ C) = (A ∪ B) ∪ C := by sorry

Source