Set_is_Subset_of_Union

Proved

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

proofwikiset-unionsubsets

The union of two sets is a superset of each $S \subseteq S \cup T$ $T \subseteq S \cup T$

Preamble

import Mathlib.Data.Set.Basic

Formal statement

theorem Set_is_Subset_of_Union {α : Type*} (S T : Set α) : S ⊆ S ∪ T ∧ T ⊆ S ∪ T := by sorry

Source