Union_is_Smallest_Superset

Proved

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

proofwikiset-unionsubsets

Let $S_1$ and $S_2$ be sets. Then $S_1 \cup S_2$ is the smallest set containing both $S_1$ and $S_2$ . That is $\paren {S_1 \subseteq T} \land \paren {S_2 \subseteq T} \iff \paren {S_1 \cup S_2} \subseteq T$

Preamble

import Mathlib.Data.Set.Basic

Formal statement

theorem Union_is_Smallest_Superset {α : Type*} (S₁ S₂ T : Set α) : (S₁ ⊆ T) ∧ (S₂ ⊆ T) ↔ (S₁ ∪ S₂) ⊆ T := by sorry

Source

https://proofwiki.org/wiki/Union_is_Smallest_Superset

View graph