Set.ext

theorem Set.ext : ∀ {α : Type u_1} {a b : Set α}, (∀ (x : α), x ∈ a ↔ x ∈ b) → a = b

The theorem `Set.ext` states that for any type `α` and any two sets `a` and `b` of type `α`, if every element `x` of type `α` belongs to `a` if and only if `x` belongs to `b`, then `a` and `b` are the same set. In other words, two sets are equal if they contain exactly the same elements.

More concisely: If two sets `a` and `b` of type `α` have the same elements, then `a = b`.