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: Closed

Proof

import Mathlib.Tactic
import Mathlib.Data.Set.Basic

theorem set_subset_trans {α : Type} {A B C : Set α} (hAB : A ⊆ B) (hBC : B ⊆ C) : A ⊆ C := by 
  intro x hx 
  apply hAB at hx 
  apply hBC at hx 
  exact hx

Back to Bounties