ZFC Integers

This file provides a construction of the integers in ZFC based on the construction of natural numbers. It follows the usual construction of integers as equivalence classes of pairs of natural numbers. The theory also comes with usual theorems and arithmetic operations on integers and wraps everything in a commutative ring structure. Finally, we show that that the ZFInt type is isomorphic to the type of elements contained in ZFSet.Int type using the Schröder-Bernstein theorem.

@[reducible, inline]

abbrev ZFSet.zrel (a b : ZFNat × ZFNat) : Prop

Imported ZFLean declaration.

Equations

• ZFSet.zrel a b = (a.1 + b.2 = a.2 + b.1)

theorem ZFSet.zrel_eq : Equivalence ZFSet.zrel

@[instance_reducible]

instance ZFSet.instSetoidZFNatZFNat : Setoid (ZFNat × ZFNat)

Equations

• ZFSet.instSetoidZFNatZFNat = { r := ZFSet.zrel, iseqv := ZFSet.zrel_eq }

@[reducible, inline]

abbrev ZFSet.ZFInt : Type (u_1 + 1)

Imported ZFLean declaration.

Equations

• ZFSet.ZFInt = Quotient ZFSet.instSetoidZFNatZFNat

def ZFSet.ZFInt.mk : ZFNat × ZFNat → ZFInt

Imported ZFLean declaration.

Equations

• ZFSet.ZFInt.mk = Quotient.mk''

@[simp]

theorem ZFSet.ZFInt.mk_eq (x : ZFNat × ZFNat) : ⟦x⟧ = mk x

@[simp]

theorem ZFSet.ZFInt.mk_out (x : ZFInt) : mk (Quotient.out x) = x

theorem ZFSet.ZFInt.eq {x y : ZFNat × ZFNat} : mk x = mk y ↔ ZFSet.zrel x y

theorem ZFSet.ZFInt.sound {x y : ZFNat × ZFNat} (h : ZFSet.zrel x y) : mk x = mk y

theorem ZFSet.ZFInt.exact {x y : ZFNat × ZFNat} : mk x = mk y → ZFSet.zrel x y

@[reducible, inline]

abbrev ZFSet.ZFInt.zero : ZFInt

Imported ZFLean declaration.

Equations

• ZFSet.ZFInt.zero = ZFSet.ZFInt.mk (0, 0)

@[reducible, inline]

abbrev ZFSet.ZFInt.one : ZFInt

Imported ZFLean declaration.

Equations

• ZFSet.ZFInt.one = ZFSet.ZFInt.mk (1, 0)

@[instance_reducible]

instance ZFSet.ZFInt.instZero : Zero ZFInt

Equations

• ZFSet.ZFInt.instZero = { zero := ZFSet.ZFInt.zero }

@[instance_reducible]

instance ZFSet.ZFInt.instOne : One ZFInt

Equations

• ZFSet.ZFInt.instOne = { one := ZFSet.ZFInt.one }

theorem ZFSet.ZFInt.zero_eq : 0 = mk (0, 0)

theorem ZFSet.ZFInt.one_eq : 1 = mk (1, 0)

theorem ZFSet.ZFInt.one_ne_zero : 1 ≠ 0

theorem ZFSet.ZFInt.mk_eq_zero_iff {n m : ZFNat} : mk (n, m) = 0 ↔ n = m

@[reducible, inline]

noncomputable abbrev ZFSet.ZFInt.add (n m : ZFInt) : ZFInt

Imported ZFLean declaration.

Equations

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

@[instance_reducible]

noncomputable instance ZFSet.ZFInt.instAdd : Add ZFInt

Equations

• ZFSet.ZFInt.instAdd = { add := ZFSet.ZFInt.add }

theorem ZFSet.ZFInt.add_eq (n m : ZFNat × ZFNat) : mk n + mk m = mk (n.1 + m.1, n.2 + m.2)

theorem ZFSet.ZFInt.add_assoc (n m k : ZFInt) : n + (m + k) = n + m + k

theorem ZFSet.ZFInt.add_comm (n m : ZFInt) : n + m = m + n

theorem ZFSet.ZFInt.add_left_comm (n m k : ZFInt) : n + (m + k) = m + (n + k)

theorem ZFSet.ZFInt.add_right_comm (n m k : ZFInt) : n + m + k = n + k + m

theorem ZFSet.ZFInt.add_zero {x : ZFInt} : x + 0 = x

theorem ZFSet.ZFInt.zero_add {x : ZFInt} : 0 + x = x

@[reducible, inline]

abbrev ZFSet.ZFInt.neg (n : ZFInt) : ZFInt

Imported ZFLean declaration.

Equations

• n.neg = Quotient.liftOn n (fun (x : ZFSet.ZFNat × ZFSet.ZFNat) => ZFSet.ZFInt.mk (x.2, x.1)) ZFSet.ZFInt.neg._proof_1

@[instance_reducible]

instance ZFSet.ZFInt.instNeg : Neg ZFInt

Equations

• ZFSet.ZFInt.instNeg = { neg := ZFSet.ZFInt.neg }

theorem ZFSet.ZFInt.neg_eq (n : ZFNat × ZFNat) : -mk n = mk (n.2, n.1)

theorem ZFSet.ZFInt.neg_neg (n : ZFInt) : - -n = n

theorem ZFSet.ZFInt.neg_zero : -0 = 0

theorem ZFSet.ZFInt.neg_inj {a b : ZFInt} : -a = -b ↔ a = b

theorem ZFSet.ZFInt.neg_eq_zero {a : ZFInt} : -a = 0 ↔ a = 0

theorem ZFSet.ZFInt.neg_ne_zero {a : ZFInt} : -a ≠ 0 ↔ a ≠ 0

theorem ZFSet.ZFInt.add_left_neg {a : ZFInt} : -a + a = 0

theorem ZFSet.ZFInt.add_right_neg (a : ZFInt) : a + -a = 0

theorem ZFSet.ZFInt.neg_eq_of_add_eq_zero {a b : ZFInt} (h : a + b = 0) : -a = b

theorem ZFSet.ZFInt.eq_neg_of_eq_neg {a b : ZFInt} (h : a = -b) : b = -a

theorem ZFSet.ZFInt.eq_neg_comm {a b : ZFInt} : a = -b ↔ b = -a

theorem ZFSet.ZFInt.neg_eq_comm {a b : ZFInt} : -a = b ↔ -b = a

theorem ZFSet.ZFInt.neg_add_cancel_left (a b : ZFInt) : -a + (a + b) = b

theorem ZFSet.ZFInt.add_neg_cancel_left (a b : ZFInt) : a + (-a + b) = b

theorem ZFSet.ZFInt.add_neg_cancel_right (a b : ZFInt) : a + b + -b = a

theorem ZFSet.ZFInt.neg_add_cancel_right (a b : ZFInt) : a + -b + b = a

theorem ZFSet.ZFInt.add_left_cancel {a b c : ZFInt} (h : a + b = a + c) : b = c

theorem ZFSet.ZFInt.neg_add {a b : ZFInt} : -(a + b) = -a + -b

@[reducible, inline]

noncomputable abbrev ZFSet.ZFInt.sub (n m : ZFInt) : ZFInt

Integer subtraction in the ZF integer model.

Equations

• n.sub m = n + -m

@[instance_reducible]

noncomputable instance ZFSet.ZFInt.instSub : Sub ZFInt

Imported ZFLean declaration.

Equations

• ZFSet.ZFInt.instSub = { sub := ZFSet.ZFInt.sub }

theorem ZFSet.ZFInt.sub_eq (n m : ZFNat × ZFNat) : mk n - mk m = mk (n.1 + m.2, n.2 + m.1)

theorem ZFSet.ZFInt.sub_eq_add_neg {a b : ZFInt} : a - b = a + -b

theorem ZFSet.ZFInt.add_neg_one (i : ZFInt) : i + -1 = i - 1

theorem ZFSet.ZFInt.sub_self (a : ZFInt) : a - a = 0

theorem ZFSet.ZFInt.sub_zero (a : ZFInt) : a - 0 = a

theorem ZFSet.ZFInt.zero_sub (a : ZFInt) : 0 - a = -a

theorem ZFSet.ZFInt.sub_eq_zero_of_eq {a b : ZFInt} (h : a = b) : a - b = 0

theorem ZFSet.ZFInt.eq_of_sub_eq_zero {a b : ZFInt} (h : a - b = 0) : a = b

theorem ZFSet.ZFInt.sub_eq_zero {a b : ZFInt} : a - b = 0 ↔ a = b

theorem ZFSet.ZFInt.sub_sub (a b c : ZFInt) : a - b - c = a - (b + c)

theorem ZFSet.ZFInt.neg_sub (a b : ZFInt) : -(a - b) = b - a

theorem ZFSet.ZFInt.sub_sub_self (a b : ZFInt) : a - (a - b) = b

theorem ZFSet.ZFInt.sub_neg (a b : ZFInt) : a - -b = a + b

theorem ZFSet.ZFInt.sub_add_cancel (a b : ZFInt) : a - b + b = a

theorem ZFSet.ZFInt.add_sub_cancel (a b : ZFInt) : a + b - b = a

theorem ZFSet.ZFInt.add_sub_assoc (a b c : ZFInt) : a + b - c = a + (b - c)

theorem ZFSet.ZFInt.sub_left_cancel (a b c : ZFInt) : a - c = b - c → a = b

theorem ZFSet.ZFInt.sub_right_cancel (a b c : ZFInt) : c - a = c - b → a = b

theorem ZFSet.ZFInt.add_eq_sub_iff {a b c : ZFInt} : a + b = c ↔ a = c - b

@[reducible, inline]

noncomputable abbrev ZFSet.ZFInt.nsmul : ℕ → ZFInt → ZFInt

Repeated addition by a natural-number scalar.

Equations

• ZFSet.ZFInt.nsmul 0 x✝ = 0
• ZFSet.ZFInt.nsmul n.succ x✝ = x✝ + ZFSet.ZFInt.nsmul n x✝

@[reducible, inline]

noncomputable abbrev ZFSet.ZFInt.zsmul (n : ℤ) (x : ZFInt) : ZFInt

Integer scalar multiplication defined using repeated addition and negation.

Equations

• ZFSet.ZFInt.zsmul (Int.ofNat n_2) x = ZFSet.ZFInt.nsmul n_2 x
• ZFSet.ZFInt.zsmul (Int.negSucc n_2) x = -ZFSet.ZFInt.nsmul (n_2 + 1) x

@[reducible, inline]

noncomputable abbrev ZFSet.ZFInt.mul (n m : ZFInt) : ZFInt

Integer multiplication in the ZF integer model.

Equations

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

@[instance_reducible]

noncomputable instance ZFSet.ZFInt.instMul : Mul ZFInt

Imported ZFLean declaration.

Equations

• ZFSet.ZFInt.instMul = { mul := ZFSet.ZFInt.mul }

theorem ZFSet.ZFInt.mul_eq (n m : ZFNat × ZFNat) : mk n * mk m = mk (n.1 * m.1 + n.2 * m.2, n.1 * m.2 + n.2 * m.1)

theorem ZFSet.ZFInt.mul_comm (n m : ZFInt) : n * m = m * n

theorem ZFSet.ZFInt.left_distrib (a b c : ZFInt) : a * (b + c) = a * b + a * c

theorem ZFSet.ZFInt.right_distrib (a b c : ZFInt) : (a + b) * c = a * c + b * c

theorem ZFSet.ZFInt.zero_mul (a : ZFInt) : 0 * a = 0

theorem ZFSet.ZFInt.mul_zero (a : ZFInt) : a * 0 = 0

theorem ZFSet.ZFInt.mul_assoc (a b c : ZFInt) : a * b * c = a * (b * c)

theorem ZFSet.ZFInt.one_mul (a : ZFInt) : 1 * a = a

theorem ZFSet.ZFInt.mul_one (a : ZFInt) : a * 1 = a

@[instance_reducible]

noncomputable instance ZFSet.ZFInt.instCommRing : CommRing ZFInt

Equations

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

@[instance_reducible]

instance ZFSet.ZFInt.intLt : LT ZFInt

Equations

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

@[instance_reducible]

instance ZFSet.ZFInt.intLe : LE ZFInt

Equations

• ZFSet.ZFInt.intLe = { le := fun (x y : ZFSet.ZFInt) => x < y ∨ x = y }

theorem ZFSet.ZFInt.lt_succ {n : ZFInt} : n < n + 1

theorem ZFSet.ZFInt.lt_trans {a b c : ZFInt} : a < b → b < c → a < c

theorem ZFSet.ZFInt.lt_irrefl {a : ZFInt} : ¬a < a

theorem ZFSet.ZFInt.lt_zero_iff {n m : ZFNat} : m < n ↔ 0 < mk (n, m)

theorem ZFSet.ZFInt.neg_one_lt_zero : -1 < 0

theorem ZFSet.ZFInt.zero_lt_one : 0 < 1

theorem ZFSet.ZFInt.le_trans {a b c : ZFInt} : a ≤ b → b ≤ c → a ≤ c

theorem ZFSet.ZFInt.le_antisymm {a b : ZFInt} : a ≤ b → b ≤ a → a = b

theorem ZFSet.ZFInt.le_total {a b : ZFInt} : a ≤ b ∨ b ≤ a

theorem ZFSet.ZFInt.lt_iff_le_not_ge {x y : ZFInt} : x < y ↔ x ≤ y ∧ ¬y ≤ x

theorem ZFSet.ZFInt.lt_neg_iff {a b : ZFInt} : a < b ↔ -b < -a

theorem ZFSet.ZFInt.le_neg_iff {a b : ZFInt} : a ≤ b ↔ -b ≤ -a

@[instance_reducible]

noncomputable instance ZFSet.ZFInt.instLinearOrder : LinearOrder ZFInt

Equations

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

@[instance_reducible]

noncomputable instance ZFSet.ZFInt.instAddCommGroup : AddCommGroup ZFInt

Equations

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

@[instance_reducible]

instance ZFSet.ZFInt.instPartialOrder : PartialOrder ZFInt

Equations

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

instance ZFSet.ZFInt.instIsOrderedAddMonoid : IsOrderedAddMonoid ZFInt

theorem ZFSet.ZFInt.ind {P : ZFNat → ZFNat → Prop} (n : ZFNat) (m : ZFNat) (zero : P 0 0) (succ_l : ∀ (n : ZFNat) (m : ZFNat), P n m → P (n + 1) m) (succ_r : ∀ (n : ZFNat) (m : ZFNat), P n m → P n (m + 1)) : P n m

theorem ZFSet.ZFInt.induction_pos {P : ZFInt → Prop} (n : ZFInt) (n_pos : 0 ≤ n) (zero : P 0) (succ : ∀ (k : ZFInt), P k → P (k + 1)) : P n

theorem ZFSet.ZFInt.induction_neg {P : ZFInt → Prop} (n : ZFInt) (n_neg : n ≤ 0) (zero : P 0) (succ : ∀ (k : ZFInt), P k → P (k - 1)) : P n

theorem ZFSet.ZFInt.induction {P : ZFInt → Prop} (n : ZFInt) (zero : P 0) (pos : ∀ (k : ZFInt), P k → P (k + 1)) (neg : ∀ (k : ZFInt), P k → P (k - 1)) : P n

theorem ZFSet.ZFInt.sign_cases {P : ZFInt → Prop} (n : ZFInt) (zero : P 0) (neg : n < 0 → P n) (pos : 0 < n → P n) : P n

theorem ZFSet.ZFInt.cases {P : ZFInt → Prop} (n : ZFInt) (pos : 0 ≤ n → P n) (neg : n < 0 → P n) : P n

theorem ZFSet.ZFInt.add_eq_add_sub_eq_sub {a b c d : ZFNat} : a + b = c + d → a - c = d - b

theorem ZFSet.ZFInt.le_of_lt_succ (n m : ZFInt) : n < m + 1 → n ≤ m

theorem ZFSet.ZFInt.lt_succ_of_le (n m : ZFInt) : n ≤ m → n < m + 1

theorem ZFSet.ZFInt.lt_succ_of_le_iff (n m : ZFInt) : n ≤ m ↔ n < m + 1

theorem ZFSet.ZFInt.intLe.dest {n m : ZFInt} : n ≤ m → ∃ (k : ZFInt), 0 ≤ k ∧ n + k = m

theorem ZFSet.ZFInt.mul_pos_pos_pos (a b : ZFInt) (ha : 0 < a) (hb : 0 < b) : 0 < a * b

theorem ZFSet.ZFInt.neg_one_mul (a : ZFInt) : -1 * a = -a

theorem ZFSet.ZFInt.neg_one_mul_neg_one : -1 * -1 = 1

theorem ZFSet.ZFInt.mul_neg_neg (a b : ZFInt) : a * b = -a * -b

theorem ZFSet.ZFInt.neg_mul_distrib (a b : ZFInt) : -(a * b) = -a * b

theorem ZFSet.ZFInt.mul_neg_neg_pos (a b : ZFInt) (ha : a < 0) (hb : b < 0) : 0 < a * b

theorem ZFSet.ZFInt.neg_flip_lt (a : ZFInt) : a < 0 ↔ 0 < -a

theorem ZFSet.ZFInt.neg_flip_le (a : ZFInt) : a ≤ 0 ↔ 0 ≤ -a

theorem ZFSet.ZFInt.mul_neg_pos_neg (a b : ZFInt) (ha : a < 0) (hb : 0 < b) : a * b < 0

theorem ZFSet.ZFInt.mul_pos_neg_neg (a b : ZFInt) (ha : 0 < a) (hb : b < 0) : a * b < 0

theorem ZFSet.ZFInt.mul_nonneg_nonneg_nonneg (a b : ZFInt) (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a * b

theorem ZFSet.ZFInt.mul_nonpos_nonneg_nonpos (a b : ZFInt) (ha : a ≤ 0) (hb : 0 ≤ b) : a * b ≤ 0

theorem ZFSet.ZFInt.mul_nonneg_nonpos_nonpos (a b : ZFInt) (ha : 0 ≤ a) (hb : b ≤ 0) : a * b ≤ 0

theorem ZFSet.ZFInt.mul_nonpos_nonpos_nonneg (a b : ZFInt) (ha : a ≤ 0) (hb : b ≤ 0) : 0 ≤ a * b

theorem ZFSet.ZFInt.mul_le_mul_left {n m : ZFInt} (k : ZFInt) (h : n ≤ m) (h' : 0 ≤ k) : k * n ≤ k * m

theorem ZFSet.ZFInt.mul_lt_mul_of_pos_left {n m k : ZFInt} (h : n < m) (hk : k > 0) : k * n < k * m

theorem ZFSet.ZFInt.pos_of_mul_pos {a b : ZFInt} (h : 0 < a * b) (ha : 0 < a) : 0 < b

theorem ZFSet.ZFInt.mul_lt_mul_of_pos_right {n m k : ZFInt} (h : n < m) (hk : k > 0) : n * k < m * k

theorem ZFSet.ZFInt.mul_pos_iff {a b : ZFInt} : 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

theorem ZFSet.ZFInt.eq_le_iff {a b : ZFInt} : a = b ↔ a ≤ b ∧ b ≤ a

theorem ZFSet.ZFInt.mul_eq_zero_iff {a b : ZFInt} : a * b = 0 ↔ a = 0 ∨ b = 0

theorem ZFSet.ZFInt.mul_eq_zero_of_ne_zero {a b : ZFInt} : a * b = 0 → a ≠ 0 → b = 0

theorem ZFSet.ZFInt.mul_left_cancel_iff {a b n : ZFInt} (h : n ≠ 0) : n * a = n * b ↔ a = b

theorem ZFSet.ZFInt.mul_right_cancel_iff {a b n : ZFInt} (h : n ≠ 0) : a * n = b * n ↔ a = b

@[instance_reducible]

noncomputable instance ZFSet.ZFInt.instCommRing_1 : CommRing ZFInt

Equations

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

@[instance_reducible]

instance ZFSet.ZFInt.instPartialOrder_1 : PartialOrder ZFInt

Equations

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

instance ZFSet.ZFInt.instIsOrderedRing : IsOrderedRing ZFInt

instance ZFSet.ZFInt.instPosMulStrictMono : PosMulStrictMono ZFInt

instance ZFSet.ZFInt.instMulPosStrictMono : MulPosStrictMono ZFInt

@[reducible, inline]

noncomputable abbrev ZFSet.Int : ZFSet.{u_1}

The ZF set of integer representatives.

Equations

• ZFSet.Int = ZFSet.Nat.prod {∅} ∪ {∅}.prod ZFSet.Nat

def ZFSet.ZFInt.ofZFNat (n : ZFNat) : ZFInt

Embeds a ZF natural number as a ZF integer.

Equations

• ZFSet.ZFInt.ofZFNat n = ZFSet.ZFInt.mk (n, 0)

noncomputable def ZFSet.ofInt : ℤ → ZFSet.{u_1}

Encodes a Lean integer as a ZF set.

Equations

• ZFSet.ofInt (Int.ofNat n_1) = ∅.pair ↑↑n_1
• ZFSet.ofInt (Int.negSucc n_1) = (↑(↑n_1 + 1)).pair ∅

noncomputable def ZFSet.toZFInt : ℤ → ZFInt

Imported ZFLean declaration.

Equations

• ZFSet.toZFInt (Int.ofNat n_1) = ZFSet.ZFInt.mk (0, ↑n_1)
• ZFSet.toZFInt (Int.negSucc n_1) = ZFSet.ZFInt.mk (↑n_1 + 1, 0)

def ZFSet.ofInt' (n : ℤ) : PSet.{u_1}

The pre-set representative of an integer in the set-theoretic encoding.

Equations

• ZFSet.ofInt' (Int.ofNat 0) = {{∅}}
• ZFSet.ofInt' (Int.ofNat n.succ) = {{∅}, {∅, PSet.ofNat n}}
• ZFSet.ofInt' (Int.negSucc n) = {{PSet.ofNat (n + 1)}, {∅, PSet.ofNat (n + 1)}}

def ZFSet.PInt' : PSet.{u_1}

A pre-set encoding of Lean integers.

Equations

• ZFSet.PInt' = { «Type» := ULift.{?u.1, 0} ℤ, Func := fun (n : ULift.{?u.1, 0} ℤ) => ZFSet.ofInt' n.down }

def ZFSet.Int' : ZFSet.{u_1}

Imported ZFLean declaration.

Equations

• ZFSet.Int' = ZFSet.mk ZFSet.PInt'

theorem ZFSet.ZFNat.mem_lift_lift_Nat (n : ℕ) : ↑↑n ∈ Nat

theorem ZFSet.mem_ofInt_Int (n : ℤ) : ofInt n ∈ Int

theorem ZFSet.sub_ofInt_singleton_Int (n : ℤ) : {ofInt n} ⊆ Int

theorem ZFSet.Int.nonempty : Int ≠ ∅

def ZFSet.π₁ (x : ZFSet.{u_1}) : ZFSet.{u_1}

First projection from the Kuratowski ordered pair encoding.

Equations

• x.π₁ = x.sInter.sUnion

noncomputable def ZFSet.π₂ (x : ZFSet.{u_1}) : ZFSet.{u_1}

Imported ZFLean declaration.

Equations

• x.π₂ = if x.sUnion \ x.sInter = ∅ then x.π₁ else (x.sUnion \ x.sInter).sUnion

@[simp]

theorem ZFSet.π₁_pair (x y : ZFSet.{u_1}) : (x.pair y).π₁ = x

@[simp]

theorem ZFSet.pair_inter {x y : ZFSet.{u_1}} : {x} ∩ {x, y} = {x}

@[simp]

theorem ZFSet.pair_union {x y : ZFSet.{u_1}} : {x} ∪ {x, y} = {x, y}

@[simp]

theorem ZFSet.pair_minus {x y : ZFSet.{u_1}} : x ≠ y → {x, y} \ {x} = {y}

@[simp]

theorem ZFSet.π₂_pair (x y : ZFSet.{u_1}) : (x.pair y).π₂ = y

theorem ZFSet.pair_eta {z A B : ZFSet.{u_1}} (h : z ∈ A.prod B) : z = z.π₁.pair z.π₂

theorem ZFSet.mem_Int_proj {x : ZFSet.{u_1}} (h : x ∈ Int) : ∃ n ∈ Nat, x.π₁ = ∅ ∧ x.π₂ = n ∨ x.π₁ = n ∧ x.π₂ = ∅

theorem ZFSet.mem_Int_proj' {x : ZFSet.{u_1}} : x ∈ Int → x.π₁ = ∅ ∧ x.π₂ ∈ Nat ∨ x.π₁ ∈ Nat ∧ x.π₂ = ∅

noncomputable def ZFSet.ZFInt.outof : ↥Int → ZFInt

Decode a member of the set-theoretic integers into its quotient representation.

Equations

• ZFSet.ZFInt.outof ⟨n, hn⟩ = if case : n.π₁ = ∅ ∧ n.π₂ ∈ ZFSet.Nat then ZFSet.ZFInt.mk (0, ⟨n.π₂, ⋯⟩) else ZFSet.ZFInt.mk (⟨n.π₁, ⋯⟩, 0)

theorem ZFSet.ZFInt.outof_inj (x y : ↥Int) : outof x = outof y → x = y

theorem ZFSet.ZFNat.mem_Nat_sub_one {n : ZFNat} : ↑(n - 1) ∈ Nat

theorem ZFSet.ZFNat.mem_Nat_sub {n m : ZFNat} : ↑(n - m) ∈ Nat

theorem ZFSet.mem_Int_empty_not_mem {x : ZFSet.{u_1}} {h : x ∈ Int} : ∅ ∉ x

Well-definedness of ZFInt with respect to ZFSet.Int

noncomputable def ZFSet.ZFInt.into (x : ZFInt) : ↥Int

This function maps ZFInt to Int by taking the first projection of the pair.

Equations

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

theorem ZFSet.ZFInt.into_inj_aux (x y : ZFInt) : x.into = y.into → Quotient.out x ≈ Quotient.out y

theorem ZFSet.ZFInt.into_inj (x y : ZFInt) : x.into = y.into → x = y

theorem ZFSet.ZFInt.into.injective : Function.Injective into

theorem ZFSet.ZFInt.outof.injective : Function.Injective outof

noncomputable def ZFSet.ZFInt.EmbeddingZFIntInt : ZFInt ↪ ↥Int

Embedding from ZF integers into the ZF integer set.

Equations

• ZFSet.ZFInt.EmbeddingZFIntInt = { toFun := ZFSet.ZFInt.into, inj' := ZFSet.ZFInt.into.injective }

noncomputable def ZFSet.ZFInt.EmbeddingIntZFInt : ↥Int ↪ ZFInt

Imported ZFLean declaration.

Equations

• ZFSet.ZFInt.EmbeddingIntZFInt = { toFun := ZFSet.ZFInt.outof, inj' := ZFSet.ZFInt.outof.injective }

@[instance_reducible]

instance ZFSet.instLTSubtypeMemInt : LT ↥Int

Imported ZFLean declaration.

Equations

• ZFSet.instLTSubtypeMemInt = { lt := fun (x y : ↥ZFSet.Int) => have f := Classical.choice ZFSet.instLTSubtypeMemInt._proof_1; f.invFun x < f.invFun y }

theorem ZFSet.ZFInt.exists_mono_bij : Nonempty { f : ZFInt → ↥Int // Function.Bijective f ∧ ∀ (x y : ZFInt), f x < f y ↔ x < y }

The Schröder-Bernstein theorem provides a bijection between ZFInt and {x // x ∈ Int}, but we need an isomorphism in order to preserve the order structure, so that the order on ZFInt and {x // x ∈ Int} is the same.

theorem ZFSet.ZFInt.exists_mono_bij_zero_eq : Nonempty { f : ZFInt → ↥Int // Function.Bijective f ∧ (∀ (x y : ZFInt), f x < f y ↔ x < y) ∧ f 0 = ⟨ofInt 0, ⋯⟩ }

@[reducible]

noncomputable def ZFSet.instEquivZFIntInt : ZFInt ≃ ↥Int

The type ZFInt correctly represents the set ZFSet.Int. NOTE: There is a constructive proof of the Schröder-Bernstein theorem stating the equi-computability of sets. It is called the Myhill isomorphism and applies to countable sets only.

Equations

• ZFSet.instEquivZFIntInt = match Classical.choice ZFSet.ZFInt.exists_mono_bij_zero_eq with | ⟨f, ⋯⟩ => Equiv.ofBijective f bij

@[instance_reducible]

noncomputable instance ZFSet.instCoeZFIntSubtypeMemInt : Coe ZFInt ↥Int

Equations

• ZFSet.instCoeZFIntSubtypeMemInt = { coe := ZFSet.instEquivZFIntInt.toFun }

@[instance_reducible]

noncomputable instance ZFSet.instCoeSubtypeMemIntZFInt : Coe (↥Int) ZFInt

Equations

• ZFSet.instCoeSubtypeMemIntZFInt = { coe := ZFSet.instEquivZFIntInt.invFun }

theorem ZFSet.instEquivZFIntInt.mono_iff (x y : ↥Int) : instEquivZFIntInt.invFun x < instEquivZFIntInt.invFun y ↔ x < y

@[instance_reducible]

instance ZFSet.instPreorderSubtypeMemInt : Preorder ↥Int

Equations

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

@[instance_reducible]

noncomputable instance ZFSet.instLinearOrderSubtypeMemInt : LinearOrder ↥Int

Equations

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