Supporting results for pointwise provable equality.

Theory $\mathsf{PA^-}$ #

source

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.addZero :

ArithmeticSentence

The add Zero construction in FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.

Equations

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

Instances For

source

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.addAssoc :

ArithmeticSentence

The add Assoc construction in FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.

Equations

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

Instances For

source

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.addComm :

ArithmeticSentence

The add Comm construction in FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.

Equations

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

Instances For

source

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.addEqOfLt :

ArithmeticSentence

The add Eq Of Lt construction in FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.

Equations

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

Instances For

source

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.zeroLe :

ArithmeticSentence

The zero Le construction in FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.

Equations

PointwiseComposition.FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.zeroLe = (“∀¹ 0 ≤ !!(PointwiseComposition.FFL.FirstOrder.Semiterm.bvar 0)”)

Instances For

source

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.zeroLtOne :

ArithmeticSentence

The zero Lt One construction in FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.

Equations

PointwiseComposition.FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.zeroLtOne = (“0 < 1 ”)

Instances For

source

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.oneLeOfZeroLt :

ArithmeticSentence

The one Le Of Zero Lt construction in FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.

Equations

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

Instances For

source

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.addLtAdd :

ArithmeticSentence

The add Lt Add construction in FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.

Equations

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

Instances For

source

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.mulZero :

ArithmeticSentence

The mul Zero construction in FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.

Equations

PointwiseComposition.FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.mulZero = (“∀¹ (!!(PointwiseComposition.FFL.FirstOrder.Semiterm.bvar 0) * 0 ) = 0 ”)

Instances For

source

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.mulOne :

ArithmeticSentence

The mul One construction in FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.

Equations

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

Instances For

source

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.mulAssoc :

ArithmeticSentence

The mul Assoc construction in FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.

Equations

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

Instances For

source

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.mulComm :

ArithmeticSentence

The mul Comm construction in FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.

Equations

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

Instances For

source

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.mulLtMul :

ArithmeticSentence

The mul Lt Mul construction in FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.

Equations

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

Instances For

source

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.distr :

ArithmeticSentence

The distr construction in FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.

Equations

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

Instances For

source

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.ltIrrefl :

ArithmeticSentence

The lt Irrefl construction in FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.

Equations

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

Instances For

source

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.ltTrans :

ArithmeticSentence

The lt Trans construction in FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.

Equations

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

Instances For

source

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.ltTri :

ArithmeticSentence

The lt Tri construction in FFL.FirstOrder.Arithmetic.PeanoMinus.Axiom.

Equations

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

Instances For

source

inductive PointwiseComposition.FFL.FirstOrder.Arithmetic.PeanoMinus :

ArithmeticTheory

Data and laws for 𝐏𝐀⁻ in 𝐏𝐀⁻.

equal (φ : Sentence ℒₒᵣ) : φ ∈ 𝐄𝐐 ℒₒᵣ → 𝐏𝐀⁻ φ
addZero : 𝐏𝐀⁻ Axiom.addZero
addAssoc : 𝐏𝐀⁻ Axiom.addAssoc
addComm : 𝐏𝐀⁻ Axiom.addComm
addEqOfLt : 𝐏𝐀⁻ Axiom.addEqOfLt
zeroLe : 𝐏𝐀⁻ Axiom.zeroLe
zeroLtOne : 𝐏𝐀⁻ Axiom.zeroLtOne
oneLeOfZeroLt : 𝐏𝐀⁻ Axiom.oneLeOfZeroLt
addLtAdd : 𝐏𝐀⁻ Axiom.addLtAdd
mulZero : 𝐏𝐀⁻ Axiom.mulZero
mulOne : 𝐏𝐀⁻ Axiom.mulOne
mulAssoc : 𝐏𝐀⁻ Axiom.mulAssoc
mulComm : 𝐏𝐀⁻ Axiom.mulComm
mulLtMul : 𝐏𝐀⁻ Axiom.mulLtMul
distr : 𝐏𝐀⁻ Axiom.distr
ltIrrefl : 𝐏𝐀⁻ Axiom.ltIrrefl
ltTrans : 𝐏𝐀⁻ Axiom.ltTrans
ltTri : 𝐏𝐀⁻ Axiom.ltTri

Instances For

source

def PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐏𝐀⁻» :

Lean.ParserDescr

The «term𝐏𝐀⁻» construction in FFL.FirstOrder.Arithmetic.

Equations

PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐏𝐀⁻» = Lean.ParserDescr.node `PointwiseComposition.FFL.FirstOrder.Arithmetic.«term𝐏𝐀⁻» 1024 (Lean.ParserDescr.symbol "𝐏𝐀⁻")

Instances For

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.PeanoMinus.finite :

Set.Finite 𝐏𝐀⁻

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.PeanoMinus.equiv_singleton_finiteConj :

𝐏𝐀⁻ ≊ {Finset.conj finite.toFinset}

source

@[simp]

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.PeanoMinus.instModelsSetStrucORingSentenceStrNat :

ℕ ↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻

source

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.PeanoMinus.instWeakerThanSentenceORingTheoryArithmeticTheoryEqAxiom :

𝐄𝐐 ℒₒᵣ ≼ 𝐏𝐀⁻

source

@[instance_reducible]

def PointwiseComposition.FFL.FirstOrder.Arithmetic.instLEModel {M : Type u_1} [ORingStructure M] :

LE M

The inst LE lean Pool construction in FFL.FirstOrder.Arithmetic.

Equations

PointwiseComposition.FFL.FirstOrder.Arithmetic.instLEModel = { le := fun (x y : M) => x = y ∨ x < y }

Instances For

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.le_def {M : Type u_1} [ORingStructure M] {x y : M} :

x ≤ y ↔ x = y ∨ x < y

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.add_zero' {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (x : M) :

x + 0 = x

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.add_assoc {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (x y z : M) :

x + y + z = x + (y + z)

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.add_comm {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (x y : M) :

x + y = y + x

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.add_eq_of_lt {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (x y : M) :

x < y → ∃ (z : M), x + z = y

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.zero_le {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (x : M) :

0 ≤ x

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.zero_lt_one {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] :

0 < 1

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.one_le_of_zero_lt {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (x : M) :

0 < x → 1 ≤ x

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.add_lt_add {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (x y z : M) :

x < y → x + z < y + z

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.mul_zero' {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (x : M) :

x * 0 = 0

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.mul_one {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (x : M) :

x * 1 = x

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.mul_assoc {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (x y z : M) :

x * y * z = x * (y * z)

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.mul_comm {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (x y : M) :

x * y = y * x

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.mul_lt_mul {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (x y z : M) :

x < y → 0 < z → x * z < y * z

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.mul_add_distr {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (x y z : M) :

x * (y + z) = x * y + x * z

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.lt_irrefl {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (x : M) :

¬x < x

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.lt_trans {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (x y z : M) :

x < y → y < z → x < z

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.lt_tri {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (x y : M) :

x < y ∨ x = y ∨ y < x

source

@[instance_reducible]

def PointwiseComposition.FFL.FirstOrder.Arithmetic.instAddCommMonoidModel {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] :

AddCommMonoid M

The inst Add Comm Monoid lean Pool construction in FFL.FirstOrder.Arithmetic.

Equations

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

Instances For

source

@[instance_reducible]

def PointwiseComposition.FFL.FirstOrder.Arithmetic.instCommMonoidModel {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] :

CommMonoid M

The inst Comm Monoid lean Pool construction in FFL.FirstOrder.Arithmetic.

Equations

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

Instances For

source

@[instance_reducible]

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.instLinearOrderModel {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] :

LinearOrder M

The inst Linear Order lean Pool construction in FFL.FirstOrder.Arithmetic.

Equations

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

Instances For

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.zero_mul {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (x : M) :

0 * x = 0

source

@[instance_reducible]

def PointwiseComposition.FFL.FirstOrder.Arithmetic.instCommSemiringModel {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] :

CommSemiring M

The inst Comm Semiring lean Pool construction in FFL.FirstOrder.Arithmetic.

Equations

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

Instances For

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.instIsStrictOrderedRing_leanPool {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] :

IsStrictOrderedRing M

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.instCanonicallyOrderedAdd_leanPool {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] :

CanonicallyOrderedAdd M

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.instIsOrderedAddMonoid_leanPool {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] :

IsOrderedAddMonoid M

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.numeral_eq_natCast_app {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (n : ℕ) :

ORingStructure.numeral n = ↑n

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.numeral_eq_natCast {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] :

ORingStructure.numeral = Nat.cast

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.not_neg {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (x : M) :

¬x < 0

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.eq_succ_of_pos {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {x : M} (h : 0 < x) :

∃ (y : M), x = y + 1

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.le_iff_lt_succ {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {x y : M} :

x ≤ y ↔ x < y + 1

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.eq_nat_of_lt_nat {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {n : ℕ} {x : M} :

x < ↑n → ∃ (m : ℕ), x = ↑m

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.eq_nat_of_le_nat {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {n : ℕ} {x : M} :

x ≤ ↑n → ∃ (m : ℕ), x = ↑m

source

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.models_R0_of_models_PeanoMinus {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] :

M↓[ℒₒᵣ ] ⊧* 𝐑₀

source

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryR0PeanoMinus :

𝐑₀ ≼ 𝐏𝐀⁻

source

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.models_RobinsonQ_of_models_PeanoMinus {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] :

M↓[ℒₒᵣ ] ⊧* 𝐐

source

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instWeakerThanSentenceORingArithmeticTheoryRobinsonQPeanoMinus :

𝐐 ≼ 𝐏𝐀⁻

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.numeral_two_eq_two {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] :

ORingStructure.numeral 2 = 2

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.numeral_three_eq_three {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] :

ORingStructure.numeral 3 = 3

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.numeral_four_eq_four {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] :

ORingStructure.numeral 4 = 4

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.lt_succ_iff_le {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {x y : M} :

x < y + 1 ↔ x ≤ y

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.lt_iff_succ_le {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {a b : M} :

a < b ↔ a + 1 ≤ b

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.succ_le_iff_lt {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {a b : M} :

a + 1 ≤ b ↔ a < b

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.pos_iff_one_le {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {a : M} :

0 < a ↔ 1 ≤ a

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.one_lt_iff_two_le {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {a : M} :

1 < a ↔ 2 ≤ a

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.not_nonpos {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (a : M) :

¬a < 0

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.lt_two_iff_le_one {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {a : M} :

a < 2 ↔ a ≤ 1

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.lt_one_iff_eq_zero {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {a : M} :

a < 1 ↔ a = 0

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.le_one_iff_eq_zero_or_one {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {a : M} :

a ≤ 1 ↔ a = 0 ∨ a = 1

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.le_two_iff_eq_zero_or_one_or_two {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {a : M} :

a ≤ 2 ↔ a = 0 ∨ a = 1 ∨ a = 2

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.le_three_iff_eq_zero_or_one_or_two_or_three {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {a : M} :

a ≤ 3 ↔ a = 0 ∨ a = 1 ∨ a = 2 ∨ a = 3

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.two_mul_two_eq_four {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] :

2 * 2 = 4

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.two_pow_two_eq_four {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] :

2 ^ 2 = 4

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.two_pos {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] :

0 < 2

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.le_mul_self {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (a : M) :

a ≤ a * a

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.le_sq {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (a : M) :

a ≤ a ^ 2

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.sq_le_sq {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {a b : M} :

a ^ 2 ≤ b ^ 2 ↔ a ≤ b

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.sq_lt_sq {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {a b : M} :

a ^ 2 < b ^ 2 ↔ a < b

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.le_mul_of_pos_right {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {a b : M} (h : 0 < b) :

a ≤ a * b

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.le_mul_of_pos_left {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {a b : M} (h : 0 < b) :

a ≤ b * a

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.le_two_mul_left {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {a : M} :

a ≤ 2 * a

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.lt_mul_of_pos_of_one_lt_right {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {a b : M} (pos : 0 < a) (h : 1 < b) :

a < a * b

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.lt_mul_of_pos_of_one_lt_left {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {a b : M} (pos : 0 < a) (h : 1 < b) :

a < b * a

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.mul_le_mul_left {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {a b c : M} (h : b ≤ c) :

a * b ≤ a * c

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.mul_le_mul_right {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {a b c : M} (h : b ≤ c) :

b * a ≤ c * a

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.lt_of_mul_lt_mul_left {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {a b c : M} (h : a * b < a * c) :

b < c

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.lt_of_mul_lt_mul_right {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {a b c : M} (h : b * a < c * a) :

b < c

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.pow_three {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (x : M) :

x ^ 3 = x * x * x

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.pow_four {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (x : M) :

x ^ 4 = x * x * x * x

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.pow_four_eq_sq_sq {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (x : M) :

x ^ 4 = (x ^ 2) ^ 2

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.instCovariantClassHMulLe_leanPool {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] :

CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.instCovariantClassHAddLe_leanPool {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] :

CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 ≤ x2

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.instCovariantClassSwapHMulLe_leanPool {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] :

CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 ≤ x2

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.one_lt_mul_self_iff {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {a : M} :

1 < a * a ↔ 1 < a

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.opos_lt_sq_pos_iff {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {a : M} :

0 < a ^ 2 ↔ 0 < a

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.one_lt_sq_iff {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {a : M} :

1 < a ^ 2 ↔ 1 < a

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.mul_self_eq_one_iff {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {a : M} :

a * a = 1 ↔ a = 1

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.sq_eq_one_iff {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {a : M} :

a ^ 2 = 1 ↔ a = 1

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.lt_square_of_lt {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {a : M} (pos : 1 < a) :

a < a ^ 2

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.two_mul_le_sq {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {i : M} (h : 2 ≤ i) :

2 * i ≤ i ^ 2

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.two_mul_le_sq_add_one {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (i : M) :

2 * i ≤ i ^ 2 + 1

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.two_mul_lt_sq {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {i : M} (h : 2 < i) :

2 * i < i ^ 2

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.succ_le_double_of_pos {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {a : M} (h : 0 < a) :

a + 1 ≤ 2 * a

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.two_mul_add_one_lt_two_mul_of_lt {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {a b : M} (h : a < b) :

2 * a + 1 < 2 * b

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.le_add_add_left {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (a b c : M) :

a ≤ a + b + c

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.le_add_add_right {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (a b c : M) :

b ≤ a + b + c

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.add_le_cancel {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (a : M) :

AddLECancellable a

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.val_npow {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (k : ℕ) (a : M) :

Semiterm.Operator.val ![a] (Semiterm.Operator.npow ℒₒᵣ k) = a ^ k

source

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instMonotoneORing {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] :

Tarski.Structure.Monotone ℒₒᵣ M

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.zero_ne_add_one {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (x : M) :

0 ≠ x + 1

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.nat_cast_inj {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {n m : ℕ} :

↑n = ↑m ↔ n = m

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.coe_coe_lt {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {n m : ℕ} :

↑n < ↑m ↔ n < m

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.coe_add_one {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] (x : ℕ) :

↑(x + 1) = ↑x + 1

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.eq_fin_of_lt_nat {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {n : ℕ} {x : M} (hx : x < ↑n) :

∃ (i : Fin n), x = ↑↑i

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.eval_ballLTSucc' {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {ξ : Type u_2} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {t : ArithmeticSemiterm ξ n} {φ : ArithmeticSemiformula ξ (n + 1)} :

(Semiformula.Eval e ε) (Semiformula.ballLTSucc t φ) ↔ ∀ x ≤ Semiterm.val e ε t, (Semiformula.Eval (x :> e) ε) φ

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.eval_bexsLTSucc' {M : Type u_1} [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] {ξ : Type u_2} {n : ℕ} {e : Fin n → M} {ε : ξ → M} {t : ArithmeticSemiterm ξ n} {φ : ArithmeticSemiformula ξ (n + 1)} :

(Semiformula.Eval e ε) (Semiformula.bexsLTSucc t φ) ↔ ∃ x ≤ Semiterm.val e ε t, (Semiformula.Eval (x :> e) ε) φ

source

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.natCast (M : Type u_1) [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] :

NatCast M

The nat Cast construction in FFL.FirstOrder.Arithmetic.

Equations

PointwiseComposition.FFL.FirstOrder.Arithmetic.natCast M = inferInstance

Instances For

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.natCast_nat (n : ℕ) :

↑n = n

source

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instStrictlyWeakerThanSentenceORingArithmeticTheoryR0PeanoMinus :

𝐑₀ ≺ 𝐏𝐀⁻

source

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.instModelsSetStrucORingSentenceStrR0 (M : Type u_2) [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* 𝐏𝐀⁻] :

M↓[ℒₒᵣ ] ⊧* 𝐑₀

Documentation

LeanPool.PointwiseComposition.Foundation.FirstOrder.Arithmetic.PeanoMinus.Basic

Theory $\mathsf{PA^-}$ #