Intersection commutativity

2/4 ~20 minlean

Prove set intersection commutativity using extensionality.

4 lines · Lean 4

import Mathlib

example {α : Type} (A B : Set α) : A ∩ B = B ∩ A := by
  sorry

Objectifs

Indices

Voir la solution

import Mathlib

example {α : Type} (A B : Set α) : A ∩ B = B ∩ A := by
  ext x
  simp [and_comm]