Definition

Difficulty: moderate — 4 definitions, 0 abbreviations, 4 lemmas, 2 theorems, 0 examples.

definition lemma theorem
legend

A property that exactly one element has picks that element out, and so serves as a definition of it. Two obligations come with such a definition. Some element has the property, and any two elements with the property are the same one. Together they license writing “the element such that”, the form of definition known as definite description.

The order of a model already defines two elements this way. Being a zero is a property exactly one element has, so a model has the zero. Being a successor of \(a\) is a property exactly one element has, so every element has the successor. Existence is where the layout of a model does the work: above \(a\) there is either nothing, and the wrap-around clause applies, or something, and then a least such element, because everything up to a witness is finite in number.

The property \(P\) defines an element: some element has \(P\), and any two elements with \(P\) are the same one.

definite-description
structure Structure.Arithmetic.Def.{u_1} {U : Type u_1} (P : U → Prop) : Prop

  • Some element has the property.

    ex : ∃ x, P x

  • Any two elements with the property are the same one.

    uniq : ∀ (x y : U), P x → P y → x = y
Show details

Outer dependencies: (none)

Lean core dependencies: Eq, Exists

Used by: Structure.Arithmetic.Recursive, Structure.Arithmetic.eq_the, Structure.Arithmetic.instDefForallForallPropFixedPointOfPredicative, Structure.Arithmetic.instDefForallForallPropFixedPointOfRecursive, Structure.Arithmetic.instDefForallForallPropFixedPointPrimitiveOfSerialOfUnivalent, Structure.Arithmetic.instDefOfSerialOfUnivalent, Structure.Arithmetic.instDefS, Structure.Arithmetic.instDefZ, Structure.Arithmetic.instPrimitiveRecursiveOfSerialOfUnivalent, Structure.Arithmetic.the, Structure.Arithmetic.the_spec

The element that \(P\) defines.

def Structure.Arithmetic.the.{u_1} {U : Type u_1} (P : U → Prop) [Structure.Arithmetic.Def P] : U
Show details 
| Structure.Arithmetic.the P = Classical.choose ⋯

Complexity: 25 (size of the value term)

Outer dependencies: Structure.Arithmetic.Def

Lean core dependencies: Classical.choose

Used by: Structure.Arithmetic.eq_the, Structure.Arithmetic.rec, Structure.Arithmetic.rec_primitive, Structure.Arithmetic.rec_spec, Structure.Arithmetic.step, Structure.Arithmetic.succ, Structure.Arithmetic.the_spec, Structure.Arithmetic.zero

The element that \(P\) defines has \(P\).

theorem Structure.Arithmetic.the_spec.{u_1} {U : Type u_1} (P : U → Prop) [Structure.Arithmetic.Def P] :
  P (Structure.Arithmetic.the P)
Show details 
fun {U} P [Structure.Arithmetic.Def P] => Classical.choose_spec Structure.Arithmetic.Def.ex

Complexity: 25 (size of the value term)

Dependencies: Structure.Arithmetic.Def, Structure.Arithmetic.the

Lean core dependencies: Classical.choose_spec

Used by: Structure.Arithmetic.S_succ, Structure.Arithmetic.Z_zero, Structure.Arithmetic.eq_the, Structure.Arithmetic.rec_spec, Structure.Arithmetic.step_spec

Anything with \(P\) is the element that \(P\) defines.

theorem Structure.Arithmetic.eq_the.{u_1} {U : Type u_1} {P : U → Prop} [Structure.Arithmetic.Def P] {x : U}
  (hx : P x) : x = Structure.Arithmetic.the P
Show details 
fun {U} {P} [Structure.Arithmetic.Def P] {x} hx =>
  Structure.Arithmetic.Def.uniq x (Structure.Arithmetic.the P) hx (Structure.Arithmetic.the_spec P)

Complexity: 45 (size of the value term)

Dependencies: Structure.Arithmetic.Def, Structure.Arithmetic.the

Proof dependencies: Structure.Arithmetic.the_spec

Lean core dependencies: Eq

Used by: Structure.Arithmetic.eq_succ_of_S, Structure.Arithmetic.fixedPoint_iter, Structure.Arithmetic.rec_primitive

Being a zero defines an element: the bottom of the order is one, and two elements that each lie below the other are the same one.

instance Structure.Arithmetic.instDefZ.{u_1} {U : Type u_1} [Structure.Arithmetic.Arith U] :
  Structure.Arithmetic.Def Structure.Arithmetic.Z
Show details 
fun {U} [Structure.Arithmetic.Arith U] =>
  { ex := Exists.intro ⊥ fun x => bot_le, uniq := fun x x_1 hx hy => le_antisymm (hx x_1) (hy x) }

Complexity: 163 (size of the value term)

Outer dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.Def, Structure.Arithmetic.Z

Mathlib dependencies: bot_le, le_antisymm

Used by: Structure.Arithmetic.Z_zero, Structure.Arithmetic.zero

The zero of the universe.

def Structure.Arithmetic.zero.{u_2} (U : Type u_2) [Structure.Arithmetic.Arith U] : U
Show details 
| Structure.Arithmetic.zero U = Structure.Arithmetic.the Structure.Arithmetic.Z

Complexity: 21 (size of the value term)

Outer dependencies: Structure.Arithmetic.Arith

Inner dependencies: Structure.Arithmetic.Z, Structure.Arithmetic.instDefZ, Structure.Arithmetic.the

Used by: Structure.Arithmetic.Exp, Structure.Arithmetic.ExpSpec, Structure.Arithmetic.Times, Structure.Arithmetic.TimesSpec, Structure.Arithmetic.Z_zero, Structure.Arithmetic.count, Structure.Arithmetic.count_succ, Structure.Arithmetic.exp_base, Structure.Arithmetic.exp_step, Structure.Arithmetic.times_base, Structure.Arithmetic.times_step

theorem Structure.Arithmetic.Z_zero.{u_1} {U : Type u_1} [Structure.Arithmetic.Arith U] :
  Structure.Arithmetic.Z (Structure.Arithmetic.zero U)
Show details 
fun {U} [Structure.Arithmetic.Arith U] => Structure.Arithmetic.the_spec Structure.Arithmetic.Z

Complexity: 21 (size of the value term)

Dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.Z, Structure.Arithmetic.zero

Proof dependencies: Structure.Arithmetic.instDefZ, Structure.Arithmetic.the_spec

Used by: Structure.Arithmetic.count_surjective

Being a successor of \(a\) defines an element. Where \(a\) is a maximum the wrap-around clause gives the zero. Elsewhere something lies above \(a\), and among the finitely many elements up to such a witness there is a least one above \(a\).

instance Structure.Arithmetic.instDefS.{u_1} {U : Type u_1} [Structure.Arithmetic.Arith U] (a : U) :
  Structure.Arithmetic.Def (Structure.Arithmetic.S a)
Show details 
fun {U} [Structure.Arithmetic.Arith U] a =>
  {
    ex :=
      if hM : Structure.Arithmetic.M a then Exists.intro ⊥ (Or.inr ⟨hM, fun x => bot_le⟩)
      else
        Exists.casesOn
          (Eq.mp
            (Eq.trans Structure.Arithmetic.instDefS._simp_1
              (congrArg Exists (funext fun x => Structure.Arithmetic.instDefS._simp_2)))
            hM)
          fun z hz =>
          Exists.casesOn
            (Set.exists_min_image {y | a < y ∧ y ≤ z} id
              (Set.Finite.subset (Structure.Arithmetic.Arith.reach z) fun y hy => hy.right)
              (Exists.intro z ⟨hz, le_rfl⟩))
            fun m h =>
            And.casesOn h fun left hmin =>
              And.casesOn left fun ham hmz =>
                Exists.intro m
                  (Or.inl
                    ⟨ham, fun w hw =>
                      Or.casesOn (le_total w z) (fun h => hmin w ⟨hw, h⟩) fun h =>
                        LE.le.trans hmz h⟩),
    uniq := fun x y a_1 =>
      Or.casesOn (motive := fun x_1 => Structure.Arithmetic.S a y → x = y) a_1
        (fun h =>
          And.casesOn (motive := fun x_1 => Structure.Arithmetic.S a y → x = y) h fun hx hx' a_2 =>
            Or.casesOn a_2 (fun h => And.casesOn h fun hy hy' => le_antisymm (hx' y hy) (hy' x hx))
              fun h => And.casesOn h fun hy hy' => absurd (hy x) (not_le.mpr hx))
        fun h =>
        And.casesOn (motive := fun x_1 => Structure.Arithmetic.S a y → x = y) h fun hx hx' a_2 =>
          Or.casesOn a_2 (fun h => And.casesOn h fun hy hy' => absurd (hx y) (not_le.mpr hy))
            fun h => And.casesOn h fun hy hy' => le_antisymm (hx' y) (hy' x) }

Complexity: 6567 (size of the value term)

Outer dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.Def, Structure.Arithmetic.S

Inner dependencies: Structure.Arithmetic.M, Structure.Arithmetic.Z

Mathlib dependencies: LinearOrder, Set, Set.Finite.subset, Set.Iic, Set.exists_min_image, bot_le, le_antisymm, le_rfl, le_total, not_le, setOf

Lean core dependencies: And, Classical.not_forall, Eq, Eq.mp, Eq.trans, Exists, Not, Or, absurd, congrArg, dite, funext, id

Used by: Structure.Arithmetic.S_succ, Structure.Arithmetic.eq_succ_of_S, Structure.Arithmetic.instSerialS, Structure.Arithmetic.instUnivalentS, Structure.Arithmetic.succ

The successor of \(a\).

def Structure.Arithmetic.succ.{u_1} {U : Type u_1} [Structure.Arithmetic.Arith U] (a : U) : U
Show details 
| Structure.Arithmetic.succ a = Structure.Arithmetic.the (Structure.Arithmetic.S a)

Complexity: 27 (size of the value term)

Outer dependencies: Structure.Arithmetic.Arith

Inner dependencies: Structure.Arithmetic.S, Structure.Arithmetic.instDefS, Structure.Arithmetic.the

Used by: Structure.Arithmetic.Exp, Structure.Arithmetic.ExpSpec, Structure.Arithmetic.S_succ, Structure.Arithmetic.count, Structure.Arithmetic.count_strictMono, Structure.Arithmetic.count_succ, Structure.Arithmetic.count_surjective, Structure.Arithmetic.eq_succ_of_S, Structure.Arithmetic.exp_base, Structure.Arithmetic.exp_step, Structure.Arithmetic.lt_succ

theorem Structure.Arithmetic.S_succ.{u_1} {U : Type u_1} [Structure.Arithmetic.Arith U] (a : U) :
  Structure.Arithmetic.S a (Structure.Arithmetic.succ a)
Show details 
fun {U} [Structure.Arithmetic.Arith U] a => Structure.Arithmetic.the_spec (Structure.Arithmetic.S a)

Complexity: 27 (size of the value term)

Dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.S, Structure.Arithmetic.succ

Proof dependencies: Structure.Arithmetic.instDefS, Structure.Arithmetic.the_spec

Used by: Structure.Arithmetic.lt_succ

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.

definitionlemmatheoremdeclared elsewheredependencyproof dependency
legend