Intersection_is_Subset

Proved

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

proofwikiset-intersectionsubsets

The intersection of two sets is a subset of each $S \cap T \subseteq S$ $S \cap T \subseteq T$

Preamble

import Mathlib.Data.Set.Basic

Formal statement

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

Source