Theorem Marketplace

Theorem Details

-- subset relation is transitive for sets

import Mathlib.Data.Set.Basic

theorem set_subset_trans {α : Type} {A B C : Set α} (hAB : A ⊆ B) (hBC : B ⊆ C) : A ⊆ C := by sorry

Bounty: 0.03 ETH

Status: Open

Submit Your Proof

Back to Bounties