Functions and relations defined in $\mathsf{PA^-}$ #

This file provides functions and relations defined in $\mathsf{PA^-}

(Modified) Subtraction #

source

theorem LO.FirstOrder.Arithmetic.sub_existsUnique {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (a b : V) :

∃! c : V, (a ≥ b → a = b + c) ∧ (a < b → c = 0)

source

noncomputable def LO.FirstOrder.Arithmetic.sub {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (a b : V) :

Equations

LO.FirstOrder.Arithmetic.sub a b = Classical.choose! ⋯

Instances For

source

@[implicit_reducible]

noncomputable def LO.FirstOrder.Arithmetic.instSub_foundation {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

Sub V

Equations

LO.FirstOrder.Arithmetic.instSub_foundation = { sub := LO.FirstOrder.Arithmetic.sub }

Instances For

source

theorem LO.FirstOrder.Arithmetic.sub_spec_of_ge {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b : V} (h : a ≥ b) :

a = b + (a - b)

source

theorem LO.FirstOrder.Arithmetic.sub_spec_of_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b : V} (h : a < b) :

a - b = 0

source

theorem LO.FirstOrder.Arithmetic.sub_eq_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b c : V} :

c = a - b ↔ (a ≥ b → a = b + c) ∧ (a < b → c = 0)

source

@[simp]

theorem LO.FirstOrder.Arithmetic.sub_le_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (a b : V) :

a - b ≤ a

source

def LO.FirstOrder.Arithmetic.subDef :

𝚺₀.Semisentence 3

Equations

One or more equations did not get rendered due to their size.

Instances For

source

instance LO.FirstOrder.Arithmetic.sub_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

𝚺₀ -Function₂ fun (x1 x2 : V) => x1 - x2 via subDef

source

instance LO.FirstOrder.Arithmetic.sub_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (ℌ : HierarchySymbol) :

ℌ-Function₂ fun (x1 x2 : V) => x1 - x2

source

instance LO.FirstOrder.Arithmetic.sub_polybounded {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

Bounded₂ fun (x1 x2 : V) => x1 - x2

source

@[simp]

theorem LO.FirstOrder.Arithmetic.sub_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (a : V) :

a - a = 0

source

theorem LO.FirstOrder.Arithmetic.sub_spec_of_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b : V} (h : a ≤ b) :

a - b = 0

source

theorem LO.FirstOrder.Arithmetic.sub_add_self_of_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b : V} (h : b ≤ a) :

a - b + b = a

source

theorem LO.FirstOrder.Arithmetic.add_tsub_self_of_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b : V} (h : b ≤ a) :

b + (a - b) = a

source

@[simp]

theorem LO.FirstOrder.Arithmetic.add_sub_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b : V} :

a + b - b = a

source

@[simp]

theorem LO.FirstOrder.Arithmetic.add_sub_self' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b : V} :

b + a - b = a

source

@[simp]

theorem LO.FirstOrder.Arithmetic.zero_sub {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (a : V) :

0 - a = 0

source

@[simp]

theorem LO.FirstOrder.Arithmetic.sub_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (a : V) :

a - 0 = a

source

theorem LO.FirstOrder.Arithmetic.sub_remove_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b c : V} (e : a = b + c) :

a - c = b

source

theorem LO.FirstOrder.Arithmetic.sub_sub {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b c : V} :

a - b - c = a - (b + c)

source

@[simp]

theorem LO.FirstOrder.Arithmetic.pos_sub_iff_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b : V} :

0 < a - b ↔ b < a

source

@[simp]

theorem LO.FirstOrder.Arithmetic.sub_eq_zero_iff_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b : V} :

a - b = 0 ↔ a ≤ b

source

instance LO.FirstOrder.Arithmetic.instOrderedSub_foundation {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

OrderedSub V

source

theorem LO.FirstOrder.Arithmetic.pred_lt_self_of_pos {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a : V} (h : 0 < a) :

a - 1 < a

source

theorem LO.FirstOrder.Arithmetic.tsub_lt_iff_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b c : V} (h : b ≤ a) :

a - b < c ↔ a < c + b

source

theorem LO.FirstOrder.Arithmetic.sub_mul {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b c : V} (h : b ≤ a) :

(a - b) * c = a * c - b * c

source

theorem LO.FirstOrder.Arithmetic.mul_sub {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b c : V} (h : b ≤ a) :

c * (a - b) = c * a - c * b

source

theorem LO.FirstOrder.Arithmetic.add_sub_of_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {b c : V} (h : c ≤ b) (a : V) :

a + b - c = a + (b - c)

source

theorem LO.FirstOrder.Arithmetic.sub_succ_add_succ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {x y : V} (h : y < x) (z : V) :

x - (y + 1) + (z + 1) = x - y + z

source

theorem LO.FirstOrder.Arithmetic.le_sub_one_of_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b : V} (h : a < b) :

a ≤ b - 1

source

@[implicit_reducible]

instance LO.FirstOrder.Arithmetic.instAddCancelCommMonoid_foundation {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

AddCancelCommMonoid V

Equations

LO.FirstOrder.Arithmetic.instAddCancelCommMonoid_foundation = { toAddCommMonoid := LO.FirstOrder.Arithmetic.instAddCommMonoid_foundation, toIsLeftCancelAdd := ⋯ }

Divisibility #

source

theorem LO.FirstOrder.Arithmetic.le_mul_self_of_pos_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b : V} (hy : 0 < b) :

a ≤ b * a

source

theorem LO.FirstOrder.Arithmetic.le_mul_self_of_pos_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b : V} (hy : 0 < b) :

a ≤ a * b

source

theorem LO.FirstOrder.Arithmetic.dvd_iff_bounded {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b : V} :

a ∣ b ↔ ∃ c ≤ b, b = a * c

source

def LO.FirstOrder.Arithmetic.dvd :

𝚺₀.Semisentence 2

Equations

One or more equations did not get rendered due to their size.

Instances For

source

instance LO.FirstOrder.Arithmetic.dvd_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

𝚺₀ -Relation fun (a b : V) => a ∣ b via dvd

source

instance LO.FirstOrder.Arithmetic.dvd_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (ℌ : HierarchySymbol) :

ℌ-Relation fun (x1 x2 : V) => x1 ∣ x2

source

def LO.FirstOrder.Arithmetic.«first_order_formula_∣_» :

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem LO.FirstOrder.Arithmetic.le_of_dvd {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b : V} (h : 0 < b) :

a ∣ b → a ≤ b

source

theorem LO.FirstOrder.Arithmetic.not_dvd_of_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b : V} (pos : 0 < b) :

b < a → ¬a ∣ b

source

theorem LO.FirstOrder.Arithmetic.dvd_antisymm {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a b : V} :

a ∣ b → b ∣ a → a = b

source

theorem LO.FirstOrder.Arithmetic.dvd_one_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a : V} :

a ∣ 1 ↔ a = 1

source

theorem LO.FirstOrder.Arithmetic.units_eq_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (u : Vˣ) :

u = 1

source

@[simp]

theorem LO.FirstOrder.Arithmetic.unit_iff_eq_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {a : V} :

IsUnit a ↔ a = 1

Prime number #

source

@[implicit_reducible]

instance LO.FirstOrder.Arithmetic.instCommMonoidWithZero_foundation {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

CommMonoidWithZero V

Equations

One or more equations did not get rendered due to their size.

source

instance LO.FirstOrder.Arithmetic.instIsCancelMulZero_foundation {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

IsCancelMulZero V

source

theorem LO.FirstOrder.Arithmetic.eq_one_or_eq_of_dvd_of_prime {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] {p a : V} (pp : Prime p) (hxp : a ∣ p) :

a = 1 ∨ a = p

source

def LO.FirstOrder.Arithmetic.IsPrime {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (a : V) :

Prop

Equations

LO.FirstOrder.Arithmetic.IsPrime a = (1 < a ∧ ∀ b ≤ a, b ∣ a → b = 1 ∨ b = a)

Instances For

source

def LO.FirstOrder.Arithmetic.isPrime :

𝚺₀.Semisentence 1

Equations

One or more equations did not get rendered due to their size.

Instances For

source

instance LO.FirstOrder.Arithmetic.isPrime_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

𝚺₀ -Predicate fun (a : V) => IsPrime a via isPrime

Minimum #

source

def LO.FirstOrder.Arithmetic.min.dfn :

𝚺₀.Semisentence 3

Equations

One or more equations did not get rendered due to their size.

Instances For

source

instance LO.FirstOrder.Arithmetic.min_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

𝚺₀ -Function₂ min via min.dfn

source

instance LO.FirstOrder.Arithmetic.min_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (ℌ : HierarchySymbol) :

ℌ-Function₂ min

source

instance LO.FirstOrder.Arithmetic.min_polybounded {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

Bounded₂ min

Maximum #

source

def LO.FirstOrder.Arithmetic.max.dfn :

𝚺₀.Semisentence 3

Equations

One or more equations did not get rendered due to their size.

Instances For

source

instance LO.FirstOrder.Arithmetic.max_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

𝚺₀ -Function₂ max via max.dfn

source

instance LO.FirstOrder.Arithmetic.max_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] (Γ : HierarchySymbol) :

Γ-Function₂ max

source

instance LO.FirstOrder.Arithmetic.max_polybounded {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ ] ⊧* 𝗣𝗔⁻] :

Bounded₂ max

Documentation

Foundation.FirstOrder.Arithmetic.PeanoMinus.Functions

Functions and relations defined in $\mathsf{PA^-}$ #

(Modified) Subtraction #

Divisibility #

Prime number #

Minimum #

Maximum #