Subset_Relation_is_Transitive

Proved

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

proofwikisubsets

The relation "is a subset of" is transitive $\paren {R \subseteq S} \land \paren {S \subseteq T} \implies R \subseteq T$

Preamble

import Mathlib.Data.Set.Basic

Formal statement

theorem Subset_Relation_is_Transitive {α : Type*} (R S T : Set α) : R ⊆ S → S ⊆ T → R ⊆ T := by sorry

Source