Operation

Difficulty: easy — 3 definitions, 3 abbreviations, 6 lemmas, 0 theorems, 0 examples.

definition abbreviation lemma

legend

The three school operations are each a primitive specification, stacked one on the next. Addition takes \(x\) as its base and steps by the successor relation. Multiplication takes the zero as its base and steps by addition with \(x\). Exponentiation takes the successor of the zero as its base and steps by multiplication with \(x\).

Each is a relation on the universe of the model rather than a function into some outside set, so the equations below read as statements about that model alone. Each stack is legitimate because the previous operation gives exactly one value at each place, which is what a step relation is asked for.

NoteStructure.Arithmetic.PlusSpec

Addition: base \(x\), stepping by the successor relation.

abbrev Structure.Arithmetic.PlusSpec.{u_1} {U : Type u_1} [Structure.Arithmetic.Arith U] (x : U) :
  (U → U → Prop) → U → U → Prop

Show details

| Structure.Arithmetic.PlusSpec x = Structure.Arithmetic.Primitive x Structure.Arithmetic.S

Complexity: 23 (size of the value term)

Outer dependencies: Structure.Arithmetic.Arith

Inner dependencies: Structure.Arithmetic.Primitive, Structure.Arithmetic.S

Used by: Structure.Arithmetic.Exp, Structure.Arithmetic.Plus, Structure.Arithmetic.Times, Structure.Arithmetic.TimesSpec, Structure.Arithmetic.exp_base, Structure.Arithmetic.exp_step, Structure.Arithmetic.times_base, Structure.Arithmetic.times_step

NoteStructure.Arithmetic.Plus

addition

def Structure.Arithmetic.Plus.{u_1} {U : Type u_1} [Structure.Arithmetic.Arith U] (x : U) : U → U → Prop

Show details

| Structure.Arithmetic.Plus x = Structure.Arithmetic.rec (Structure.Arithmetic.PlusSpec x)

Complexity: 29 (size of the value term)

Outer dependencies: Structure.Arithmetic.Arith

Inner dependencies: Structure.Arithmetic.PlusSpec, Structure.Arithmetic.S, Structure.Arithmetic.instPrimitiveRecursiveOfSerialOfUnivalent, Structure.Arithmetic.instSerialS, Structure.Arithmetic.instUnivalentS, Structure.Arithmetic.rec

Used by: Structure.Arithmetic.plus_base, Structure.Arithmetic.plus_step, Structure.Arithmetic.times_step

NoteStructure.Arithmetic.TimesSpec

Multiplication: base the zero, stepping by addition with \(x\).

abbrev Structure.Arithmetic.TimesSpec.{u_1} {U : Type u_1} [Structure.Arithmetic.Arith U] (x : U) :
  (U → U → Prop) → U → U → Prop

Show details

| Structure.Arithmetic.TimesSpec x =
  Structure.Arithmetic.Primitive (Structure.Arithmetic.zero U)
    (Structure.Arithmetic.rec (Structure.Arithmetic.PlusSpec x))

Complexity: 43 (size of the value term)

Outer dependencies: Structure.Arithmetic.Arith

Inner dependencies: Structure.Arithmetic.PlusSpec, Structure.Arithmetic.Primitive, Structure.Arithmetic.rec, Structure.Arithmetic.zero

Used by: Structure.Arithmetic.Exp, Structure.Arithmetic.ExpSpec, Structure.Arithmetic.Times, Structure.Arithmetic.exp_base, Structure.Arithmetic.exp_step

NoteStructure.Arithmetic.Times

multiplication

def Structure.Arithmetic.Times.{u_1} {U : Type u_1} [Structure.Arithmetic.Arith U] (x : U) :
  U → U → Prop

Show details

| Structure.Arithmetic.Times x = Structure.Arithmetic.rec (Structure.Arithmetic.TimesSpec x)

Complexity: 29 (size of the value term)

Outer dependencies: Structure.Arithmetic.Arith

Inner dependencies: Structure.Arithmetic.PlusSpec, Structure.Arithmetic.S, Structure.Arithmetic.TimesSpec, Structure.Arithmetic.instPrimitiveRecursiveOfSerialOfUnivalent, Structure.Arithmetic.instSerialRecPrimitive, Structure.Arithmetic.instSerialS, Structure.Arithmetic.instUnivalentRecPrimitive, Structure.Arithmetic.instUnivalentS, Structure.Arithmetic.rec, Structure.Arithmetic.zero

Used by: Structure.Arithmetic.exp_step, Structure.Arithmetic.times_base, Structure.Arithmetic.times_step

NoteStructure.Arithmetic.ExpSpec

Exponentiation: base the successor of the zero, stepping by multiplication with \(x\).

abbrev Structure.Arithmetic.ExpSpec.{u_1} {U : Type u_1} [Structure.Arithmetic.Arith U] (x : U) :
  (U → U → Prop) → U → U → Prop

Show details

| Structure.Arithmetic.ExpSpec x =
  Structure.Arithmetic.Primitive (Structure.Arithmetic.succ (Structure.Arithmetic.zero U))
    (Structure.Arithmetic.rec (Structure.Arithmetic.TimesSpec x))

Complexity: 49 (size of the value term)

Outer dependencies: Structure.Arithmetic.Arith

Inner dependencies: Structure.Arithmetic.Primitive, Structure.Arithmetic.TimesSpec, Structure.Arithmetic.rec, Structure.Arithmetic.succ, Structure.Arithmetic.zero

Used by: Structure.Arithmetic.Exp

NoteStructure.Arithmetic.Exp

exponentiation

def Structure.Arithmetic.Exp.{u_1} {U : Type u_1} [Structure.Arithmetic.Arith U] (x : U) : U → U → Prop

Show details

| Structure.Arithmetic.Exp x = Structure.Arithmetic.rec (Structure.Arithmetic.ExpSpec x)

Complexity: 29 (size of the value term)

Outer dependencies: Structure.Arithmetic.Arith

Inner dependencies: Structure.Arithmetic.ExpSpec, Structure.Arithmetic.PlusSpec, Structure.Arithmetic.S, Structure.Arithmetic.TimesSpec, Structure.Arithmetic.instPrimitiveRecursiveOfSerialOfUnivalent, Structure.Arithmetic.instSerialRecPrimitive, Structure.Arithmetic.instSerialS, Structure.Arithmetic.instUnivalentRecPrimitive, Structure.Arithmetic.instUnivalentS, Structure.Arithmetic.rec, Structure.Arithmetic.succ, Structure.Arithmetic.zero

Used by: Structure.Arithmetic.exp_base, Structure.Arithmetic.exp_step

TipStructure.Arithmetic.plus_base

\(x + 0 = x\).

theorem Structure.Arithmetic.plus_base.{u_1} {U : Type u_1} [Structure.Arithmetic.Arith U] {x a v : U}
  (ha : Structure.Arithmetic.Z a) : Structure.Arithmetic.Plus x a v ↔ v = x

Show details

fun {U} [Structure.Arithmetic.Arith U] {x a v} ha =>
  Structure.Arithmetic.rec_base x Structure.Arithmetic.S ha

Complexity: 53 (size of the value term)

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

Proof dependencies: Structure.Arithmetic.S, Structure.Arithmetic.instSerialS, Structure.Arithmetic.instUnivalentS, Structure.Arithmetic.rec_base

Lean core dependencies: Eq, Iff

Used by: (none)

TipStructure.Arithmetic.plus_step

\(x + (u + 1) = (x + u) + 1\).

theorem Structure.Arithmetic.plus_step.{u_1} {U : Type u_1} [Structure.Arithmetic.Arith U] {x a u v : U}
  (ha : ¬Structure.Arithmetic.Z a) (hu : Structure.Arithmetic.S u a) :
  Structure.Arithmetic.Plus x a v ↔
    ∃ w, Structure.Arithmetic.Plus x u w ∧ Structure.Arithmetic.S w v

Show details

fun {U} [Structure.Arithmetic.Arith U] {x a u v} ha hu =>
  Structure.Arithmetic.rec_step x Structure.Arithmetic.S ha hu

Complexity: 71 (size of the value term)

Dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.Plus, Structure.Arithmetic.S, Structure.Arithmetic.Z

Proof dependencies: Structure.Arithmetic.instSerialS, Structure.Arithmetic.instUnivalentS, Structure.Arithmetic.rec_step

Lean core dependencies: And, Exists, Iff, Not

Used by: (none)

TipStructure.Arithmetic.times_base

\(x \cdot 0 = 0\).

theorem Structure.Arithmetic.times_base.{u_1} {U : Type u_1} [Structure.Arithmetic.Arith U] {x a v : U}
  (ha : Structure.Arithmetic.Z a) :
  Structure.Arithmetic.Times x a v ↔ v = Structure.Arithmetic.zero U

Show details

fun {U} [Structure.Arithmetic.Arith U] {x a v} ha =>
  Structure.Arithmetic.rec_base (Structure.Arithmetic.zero U)
    (Structure.Arithmetic.rec (Structure.Arithmetic.PlusSpec x)) ha

Complexity: 117 (size of the value term)

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

Proof dependencies: Structure.Arithmetic.PlusSpec, Structure.Arithmetic.S, Structure.Arithmetic.instSerialRecPrimitive, Structure.Arithmetic.instSerialS, Structure.Arithmetic.instUnivalentRecPrimitive, Structure.Arithmetic.instUnivalentS, Structure.Arithmetic.rec, Structure.Arithmetic.rec_base

Lean core dependencies: Eq, Iff

Used by: (none)

TipStructure.Arithmetic.times_step

\(x \cdot (u + 1) = x \cdot u + x\).

theorem Structure.Arithmetic.times_step.{u_1} {U : Type u_1} [Structure.Arithmetic.Arith U] {x a u v : U}
  (ha : ¬Structure.Arithmetic.Z a) (hu : Structure.Arithmetic.S u a) :
  Structure.Arithmetic.Times x a v ↔
    ∃ w, Structure.Arithmetic.Times x u w ∧ Structure.Arithmetic.Plus x w v

Show details

fun {U} [Structure.Arithmetic.Arith U] {x a u v} ha hu =>
  Structure.Arithmetic.rec_step (Structure.Arithmetic.zero U)
    (Structure.Arithmetic.rec (Structure.Arithmetic.PlusSpec x)) ha hu

Complexity: 135 (size of the value term)

Dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.Plus, Structure.Arithmetic.S, Structure.Arithmetic.Times, Structure.Arithmetic.Z

Proof dependencies: Structure.Arithmetic.PlusSpec, Structure.Arithmetic.instSerialRecPrimitive, Structure.Arithmetic.instSerialS, Structure.Arithmetic.instUnivalentRecPrimitive, Structure.Arithmetic.instUnivalentS, Structure.Arithmetic.rec, Structure.Arithmetic.rec_step, Structure.Arithmetic.zero

Lean core dependencies: And, Exists, Iff, Not

Used by: (none)

TipStructure.Arithmetic.exp_base

\(x^0 = 1\).

theorem Structure.Arithmetic.exp_base.{u_1} {U : Type u_1} [Structure.Arithmetic.Arith U] {x a v : U}
  (ha : Structure.Arithmetic.Z a) :
  Structure.Arithmetic.Exp x a v ↔ v = Structure.Arithmetic.succ (Structure.Arithmetic.zero U)

Show details

fun {U} [Structure.Arithmetic.Arith U] {x a v} ha =>
  Structure.Arithmetic.rec_base (Structure.Arithmetic.succ (Structure.Arithmetic.zero U))
    (Structure.Arithmetic.rec (Structure.Arithmetic.TimesSpec x)) ha

Complexity: 251 (size of the value term)

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

Proof dependencies: Structure.Arithmetic.PlusSpec, Structure.Arithmetic.S, Structure.Arithmetic.TimesSpec, Structure.Arithmetic.instSerialRecPrimitive, Structure.Arithmetic.instSerialS, Structure.Arithmetic.instUnivalentRecPrimitive, Structure.Arithmetic.instUnivalentS, Structure.Arithmetic.rec, Structure.Arithmetic.rec_base

Lean core dependencies: Eq, Iff

Used by: (none)

TipStructure.Arithmetic.exp_step

\(x^{u + 1} = x^u \cdot x\).

theorem Structure.Arithmetic.exp_step.{u_1} {U : Type u_1} [Structure.Arithmetic.Arith U] {x a u v : U}
  (ha : ¬Structure.Arithmetic.Z a) (hu : Structure.Arithmetic.S u a) :
  Structure.Arithmetic.Exp x a v ↔
    ∃ w, Structure.Arithmetic.Exp x u w ∧ Structure.Arithmetic.Times x w v

Show details

fun {U} [Structure.Arithmetic.Arith U] {x a u v} ha hu =>
  Structure.Arithmetic.rec_step (Structure.Arithmetic.succ (Structure.Arithmetic.zero U))
    (Structure.Arithmetic.rec (Structure.Arithmetic.TimesSpec x)) ha hu

Complexity: 269 (size of the value term)

Dependencies: Structure.Arithmetic.Arith, Structure.Arithmetic.Exp, Structure.Arithmetic.S, Structure.Arithmetic.Times, Structure.Arithmetic.Z

Proof dependencies: Structure.Arithmetic.PlusSpec, Structure.Arithmetic.TimesSpec, Structure.Arithmetic.instSerialRecPrimitive, Structure.Arithmetic.instSerialS, Structure.Arithmetic.instUnivalentRecPrimitive, Structure.Arithmetic.instUnivalentS, Structure.Arithmetic.rec, Structure.Arithmetic.rec_step, Structure.Arithmetic.succ, Structure.Arithmetic.zero

Lean core dependencies: And, Exists, Iff, Not

Used by: (none)

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.

definitionabbreviationlemmadeclared elsewheredependencyproof dependency

legend