Grace/Cumulus/Nat/Least.g17

Open in Workbench Download source

Imports

Order · Set.Core

Declarations

Source

1-- Least members of inhabited sets of natural numbers, in ZF.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67-- Copyright (c) 2026 Grant Passmore. Apache License 2.0.8module Grace.Cumulus.Nat.Least9import Order10import Set.Core1112-- Minimality is expressed by membership here; the public order law below13-- hides the von Neumann representation. No arbitrary choice is involved.14defunique leastNatural (S : Set) (n ∈ ℕ) :=15  n ∈ S ∧ (∀ m ∈ n, ¬m ∈ S)16requires inhabited : Nonempty(S)17requires naturals : S ⊆ ℕ18proof19  have nonempty := Nonempty.ne_empty at S with inhabited20  obtain ⟨n, member, minimal⟩ := set.foundation at S with nonempty21  unfold Subset at naturals22  have natural := naturals with n, member23  witness n24  refine ⟨natural, member, minimal⟩25uniqueness26  intros n nNatural nData k kNatural kData27  rcases nData with ⟨nMember, nMinimal⟩28  rcases kData with ⟨kMember, kMinimal⟩29  have nNat := nat.omega.backward at n with nNatural30  have kNat := nat.omega.backward at k with kNatural31  have comparison := Less.trichotomy at n, k with *32  cases comparison with before | rest33  . have inside := membership.of_Less at n, k with *, before34    exfalso35    exact kMinimal with n, inside, nMember36  . cases rest with same | after37    . exact same38    . have inside := membership.of_Less at k, n with *, after39      exfalso40      exact nMinimal with k, inside, kMember4142theorem leastNatural.member (S : Set)43  requires inhabited : Nonempty(S)44  requires naturals : S ⊆ ℕ45  shows leastNatural(S) ∈ S46proof47  simp [leastNatural.selected]4849theorem leastNatural.least (S : Set, m : Nat)50  requires inhabited : Nonempty(S)51  requires naturals : S ⊆ ℕ52  requires member : m ∈ S53  shows leastNatural(S) ≤ m54proof55  have selected := leastNatural.selected at S with *56  rcases selected with ⟨natural, chosen, minimal⟩57  have chosenNat := nat.omega.backward with natural58  by_contra notLeast59  have before := Less.of_not_LessEqual with *60  have inside := membership.of_Less with *, before61  exact minimal with m, inside, member62