Extremal Argument

Derive results from properties of minimal/maximal elements.

The Key Insight

The minimal/maximal element can't be made "more extreme," which constrains what's possible.

Step 1: Define the Extreme Element

• • What set are we considering?
• • What property defines the set?
• • Are we taking min or max?
• • Why does this extreme element exist? (set is finite, or well-ordered)

Let S = { x : x has property P }
Assume S is non-empty.
Let x₀ = min(S) or max(S).

Step 2: Use Extremality

The key: x₀ cannot be improved.

• • If x₀ is minimal: nothing smaller has property P
• • If x₀ is maximal: nothing larger has property P

This means:

• •Any x < x₀ must fail property P
• •This failure gives us information

Step 3: Derive Consequences

Common patterns:

• •Minimal counterexample → derive contradiction → no counterexamples exist
• •Minimal element with property → characterize it precisely
• •Maximal structure → can't add more without breaking property

Step 4: Lean Formalization

Key concepts:

• •Nat.find - find smallest n with property (if exists)
• •Finset.min' / max' - min/max of finite set
• •Well-founded induction

-- Minimal counterexample pattern
theorem no_counterexample (P : ℕ → Prop) :
    (∀ n, (∀ k < n, P k) → P n) → ∀ n, P n := by
  intro h
  intro n
  induction n using Nat.strong_induction_on with
  | _ n ih => exact h n ih

Classic Examples

Infinite primes (extremal version):

• •Suppose only finitely many primes
• •Let P = largest prime
• •Consider N = (product of all primes) + 1
• •N has a prime factor p
• •p must be in our list (only primes)
• •But p divides N and divides product, so p divides 1
• •Contradiction

Minimal criminal:

• •Suppose theorem false for some n
• •Let n₀ = smallest counterexample
• •Prove n₀ can't be minimal (derive contradiction)
• •Therefore no counterexample exists