Set inclusion transitivity

2/4 ~15 minlean

Prove transitivity of subset inclusion elementwise.

5 lines · Lean 4

import Mathlib

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

Objectifs

Indices

Voir la solution

import Mathlib

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