theorem SetTheory.de_morgan_laws {α : Type u_1} (A B C : Set α) : (B ∪ C)ᶜ = Bᶜ ∩ Cᶜ ∧ (B ∩ C)ᶜ = Bᶜ ∪ Cᶜ ∧ A \ (B ∪ C) = A \ B ∩ (A \ C) ∧ A \ (B ∩ C) = A \ B ∪ A \ C

De Morgan's Laws. For sets A, B, C: the complement of a union is the intersection of complements, the complement of an intersection is the union of complements, and the analogous identities for set differences: A \ (B ∪ C) = (A \ B) ∩ (A \ C) and A \ (B ∩ C) = (A \ B) ∪ (A \ C).

theorem SetTheory.well_ordering_nat (S : Set ℕ) (hS : S.Nonempty) : ∃ x ∈ S, ∀ y ∈ S, x ≤ y

Well-ordering of ℕ. Every nonempty subset S ⊆ ℕ contains a least element, that is, there exists x ∈ S such that x ≤ y for all y ∈ S.

theorem SetTheory.induction_principle (P : ℕ → Prop) (base : P 1) (step : ∀ (m : ℕ), P m → P (m + 1)) (n : ℕ) : n ≥ 1 → P n

Principle of mathematical induction (starting at 1). If P 1 holds and P m → P (m + 1) for all m, then P n holds for every natural number n ≥ 1.

theorem SetTheory.set_relations {α : Type u_1} (A B : Set α) : (A ⊆ B ↔ ∀ a ∈ A, a ∈ B) ∧ (A = B ↔ A ⊆ B ∧ B ⊆ A) ∧ (A ⊂ B ↔ A ⊆ B ∧ A ≠ B)

Basic set relations. A ⊆ B means every element of A lies in B; A = B is equivalent to mutual inclusion A ⊆ B and B ⊆ A; and A ⊂ B (proper subset) is equivalent to A ⊆ B together with A ≠ B.