ZFC Natural numbers

This file defines the natural numbers in ZF set theory. The definition is based on the construction of the Von Neumann ordinals, where each natural number is represented as the set of all smaller natural numbers.

The set of all natural numbers is defined as the smallest inductive set. Because of the axiom of separation, the definition relies on the existence of an infinite set, which is provided by the someInf constant. It can be shown that the choice of someInf does not affect the definition of the natural numbers and leads to isomorphic definitions.

The file also includes the definition of the ZFNat type for ZF natural numbers, and provides various properties and usual arithmetic operations on natural numbers.

Preliminary definitions

def ZFSet.transitive (x : ZFSet.{u_1}) : Prop

A set x is transitive if every element of x is a subset of x: ∀ y ∈ x, y ⊆ x.

Equations

• x.transitive = ∀ y ∈ x, y ⊆ x

def ZFSet.inductiveSet (E : ZFSet.{u_1}) : Prop

An inductive set is defined as a set that contains the empty set ∅ and is closed under successor.

The "successor" of a set x is defined as the insertion of x into itself.

Equations

• E.inductiveSet = (∅ ∈ E ∧ ∀ n ∈ E, insert n n ∈ E)

theorem ZFSet.trans_imp_insert_trans {x : ZFSet.{u_1}} : x.transitive → (insert x x).transitive

theorem ZFSet.inductive_sep {S : ZFSet.{u_1}} (P : ZFSet.{u_1} → Prop) (ind : S.inductiveSet) (h₀ : P ∅) (h₁ : ∀ n ∈ S, P n → P (insert n n)) : (ZFSet.sep P S).inductiveSet

theorem ZFSet.inductive_imp_transitive {E : ZFSet.{u_1}} (h : E.inductiveSet) : (ZFSet.sep transitive E).inductiveSet

def ZFSet.termω : Lean.ParserDescr

Imported ZFLean declaration.

Equations

• ZFSet.termω = Lean.ParserDescr.node `ZFSet.termω 1024 (Lean.ParserDescr.symbol "ω")

theorem ZFSet.omega_inductive : ω.inductiveSet

The first Von Neumann ordinal ω is an inductive set.

@[reducible, inline]

noncomputable abbrev ZFSet.someInf : ZFSet.{u_1}

Witness for an infinite set, meant to be used for definitional purpose only.

Equations

• ZFSet.someInf = Classical.choose ZFSet.someInf._proof_1

Natural numbers

noncomputable def ZFSet.Nat : ZFSet.{u_1}

The set of natural numbers Nat is defined as the smallest inductive set. This definition avoids the use of ω, even though ω may be thought of as ℕ.

Equations

• ZFSet.Nat = (ZFSet.sep ZFSet.inductiveSet ZFSet.someInf.powerset).sInter

@[reducible, inline]

abbrev ZFSet.ZFNat : Type (u_1 + 1)

The type of natural numbers ZFNat is defined as the subtype of Nat.

Equations

• ZFSet.ZFNat = ↥ZFSet.Nat

theorem ZFSet.ZFNat.Nat_subset_some_inf : Nat ⊆ someInf

Nat is an infinite inductive set.

theorem ZFSet.ZFNat.zero_in_Nat : ∅ ∈ Nat

@[instance_reducible]

instance ZFSet.ZFNat.natZero : Zero ZFNat

Equations

• ZFSet.ZFNat.natZero = { zero := ⟨∅, ZFSet.ZFNat.zero_in_Nat⟩ }

theorem ZFSet.ZFNat.natZero_eq : 0 = ⟨∅, zero_in_Nat⟩

@[instance_reducible]

instance ZFSet.ZFNat.natLt : LT ZFNat

Equations

• ZFSet.ZFNat.natLt = { lt := fun (x y : ZFSet.ZFNat) => ↑x ∈ ↑y }

@[instance_reducible]

instance ZFSet.ZFNat.natLe : LE ZFNat

Equations

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

theorem ZFSet.ZFNat.not_lt_zero {n : ZFNat} : ¬n < 0

theorem ZFSet.ZFNat.zero_lt_ne_zero {n : ZFNat} : 0 < n → n ≠ 0

theorem ZFSet.ZFNat.zero_mem_inductive {a : ZFSet.{u_1}} (h : a.inductiveSet) : ↑0 ∈ a

Any inductive set contains zero.

theorem ZFSet.ZFNat.insert_mem_inductive {a n : ZFSet.{u_1}} (h : a.inductiveSet) (h' : n ∈ a) : insert n n ∈ a

Any inductive set containing an element also contains its successor.

theorem ZFSet.ZFNat.some_inf_powerset_sep_inductive_nonempty : (ZFSet.sep inductiveSet someInf.powerset).Nonempty

theorem ZFSet.ZFNat.inductive_subset_some_inf_contains_Nat {a : ZFSet.{u_1}} (h : a.inductiveSet) (h' : a ⊆ someInf) : Nat ⊆ a

Any inductive set is a subset of someInf.

theorem ZFSet.ZFNat.succ_mem_Nat' {n : ZFSet.{u_1}} (h : n ∈ Nat) : insert n n ∈ Nat

def ZFSet.ZFNat.succ (n : ZFNat) : ZFNat

The successor function succ is build from the insertion of a set into itself embedded into the ZFNat type.

Equations

• ZFSet.ZFNat.succ ⟨n_2, h⟩ = ⟨insert n_2 n_2, ⋯⟩

@[instance_reducible]

instance ZFSet.ZFNat.natOne : One ZFNat

Equations

• ZFSet.ZFNat.natOne = { one := ZFSet.ZFNat.succ 0 }

theorem ZFSet.ZFNat.natOne_eq : 1 = succ 0

theorem ZFSet.ZFNat.succ_ne_zero (n : ZFNat) : n.succ ≠ 0

theorem ZFSet.ZFNat.succ_inj_aux {m n a : ZFSet.{u_1}} (h : insert m m = insert n n) (h' : a ∈ m) : a ∈ n

theorem ZFSet.ZFNat.succ_inj_aux' {m n : ZFSet.{u_1}} (h : insert m m = insert n n) : m = n

theorem ZFSet.ZFNat.succ_inj {m n : ZFNat} (h : m.succ = n.succ) : m = n

theorem ZFSet.ZFNat.sep_of_ind_is_ind (P : ZFSet.{u_1} → Prop) {a : ZFSet.{u_1}} (h : a.inductiveSet) (h₀ : P ∅) (ih : ∀ n ∈ a, P n → P (insert n n)) : (ZFSet.sep P a).inductiveSet

Any inductive set a separated by an inductive predicate P is inductive.

Recursion on natural numbers

theorem ZFSet.ZFNat.succ_subrelation_mem' : Subrelation (fun (x y : ZFSet.{u_1}) => insert x x = y) fun (x y : ZFSet.{u_1}) => x ∈ y

theorem ZFSet.ZFNat.succ_wf' : WellFounded fun (x y : ZFSet.{u_1}) => insert x x = y

theorem ZFSet.ZFNat.mem_wf' : WellFounded fun (x1 x2 : ZFNat) => ↑x1 ∈ ↑x2

theorem ZFSet.ZFNat.succ_subrelation_mem : Subrelation (fun (x1 x2 : ZFNat) => x1.succ = x2) fun (x1 x2 : ZFNat) => ↑x1 ∈ ↑x2

The relation built over the successor function is a subrelation of the membership relation.

theorem ZFSet.ZFNat.succ_wf : WellFounded fun (x1 x2 : ZFNat) => x1.succ = x2

theorem ZFSet.ZFNat.ind {P : ZFSet.{u_1} → Prop} (n : ZFSet.{u_1}) (h : n ∈ Nat) (zero : P ∅) (succ : ∀ n ∈ Nat, P n → P (insert n n)) : P n

The induction principle for sets in Nat. This principle is meant to be used for definitional purposes only.

theorem ZFSet.ZFNat.induction {P : ZFNat → Prop} (n : ZFNat) (zero : P 0) (succ : ∀ (n : ZFNat), P n → P n.succ) : P n

The (weak) induction principle for natural numbers.

theorem ZFSet.ZFNat.cases {P : ZFNat → Prop} (n : ZFNat) (zero : P 0) (succ : ∀ (n : ZFNat), P n.succ) : P n

theorem ZFSet.ZFNat.every_nat_transitive {n : ZFSet.{u_1}} (h : n ∈ Nat) : n.transitive

theorem ZFSet.ZFNat.lt_succ {n : ZFNat} : n < n.succ

theorem ZFSet.ZFNat.le_succ {n : ZFNat} : n ≤ n.succ

theorem ZFSet.ZFNat.lt_trans {x y z : ZFNat} : x < y → y < z → x < z

theorem ZFSet.ZFNat.lt_irrefl {n : ZFNat} : ¬n < n

theorem ZFSet.ZFNat.lt_imp_ne {n m : ZFNat} : n < m → n ≠ m

theorem ZFSet.ZFNat.le_trans {x y z : ZFNat} : x ≤ y → y ≤ z → x ≤ z

theorem ZFSet.ZFNat.le_antisymm {x y : ZFNat} : x ≤ y → y ≤ x → x = y

theorem ZFSet.ZFNat.lt_le_iff {n m : ZFNat} : n ≤ m ↔ n < m.succ

theorem ZFSet.ZFNat.lt_mono {x y : ZFNat} : x < y → x.succ < y.succ

theorem ZFSet.ZFNat.succ_lt_mono {x y : ZFNat} : x.succ < y.succ → x < y

theorem ZFSet.ZFNat.le_mono {x y : ZFNat} : x ≤ y → x.succ ≤ y.succ

theorem ZFSet.ZFNat.succ_le_mono {x y : ZFNat} : x.succ ≤ y.succ → x ≤ y

theorem ZFSet.ZFNat.le_lt_iff {n m : ZFNat} : n.succ ≤ m ↔ n < m

theorem ZFSet.ZFNat.le_total {x y : ZFNat} : x ≤ y ∨ y ≤ x

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

theorem ZFSet.ZFNat.strong_induction {P : ZFNat → Prop} (n : ZFNat) (ind : ∀ (n : ZFNat), (∀ m < n, P m) → P n) : P n

The (strong) induction principle for natural numbers.

theorem ZFSet.ZFNat.mem_Nat_of_mem_mem_Nat {n m : ZFSet.{u_1}} (hn : n ∈ Nat) : m ∈ n → m ∈ Nat

theorem ZFSet.ZFNat.not_zero_imp_succ {n : ZFNat} : n ≠ 0 → ∃ (m : ZFNat), n = m.succ

theorem ZFSet.ZFNat.sUnion_insert_nat {x : ZFSet.{u_1}} (h : x ∈ Nat) : (insert x x).sUnion = x

theorem ZFSet.ZFNat.pred_in_Nat' ⦃x : ZFSet.{u_1}⦄ (h : x ∈ Nat) : x.sUnion ∈ Nat

def ZFSet.ZFNat.pred (x : ZFNat) : ZFNat

The predecessor function on natural numbers, defined directly as the union of a set.

Equations

• x.pred = Subtype.map ZFSet.sUnion ZFSet.ZFNat.pred_in_Nat' x

theorem ZFSet.ZFNat.pred_eq (n : ZFNat) : n.pred = ⟨(↑n).sUnion, ⋯⟩

@[simp]

theorem ZFSet.ZFNat.pred_zero : pred 0 = 0

@[simp]

theorem ZFSet.ZFNat.pred_one : pred 1 = 0

@[simp]

theorem ZFSet.ZFNat.pred_succ {n : ZFNat} : n.succ.pred = n

@[simp]

theorem ZFSet.ZFNat.succ_pred {n : ZFNat} (h : n ≠ 0) : n.pred.succ = n

noncomputable def ZFSet.ZFNat.rec' {motive : ZFSet.{u_1} → Sort u} (n : ZFSet.{u_1}) (h : n ∈ Nat) (zero : motive ∅) (succ : (x : ZFSet.{u_1}) → x ∈ Nat → motive x → motive (insert x x)) : motive n

The recursion principle for sets in Nat. This principle is meant to be used for definitional purposes only.

Equations

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

theorem ZFSet.ZFNat.rec'_zero {motive : ZFSet.{u_1} → Sort u} (zero : motive ∅) (succ : (x : ZFSet.{u_1}) → x ∈ Nat → motive x → motive (insert x x)) : rec' ∅ zero_in_Nat zero succ = zero

Provides the base case of the recursion principle for sets in Nat.

theorem ZFSet.ZFNat.rec'_succ {motive : ZFSet.{u_1} → Sort u} (n : ZFSet.{u_1}) (n_Nat : n ∈ Nat) (zero : motive ∅) (succ : (x : ZFSet.{u_1}) → x ∈ Nat → motive x → motive (insert x x)) : rec' (insert n n) ⋯ zero succ = succ n n_Nat (rec' n n_Nat zero succ)

Provides the inductive step of the recursion principle for sets in Nat.

noncomputable def ZFSet.ZFNat.rec {motive : ZFNat → Sort u} (n : ZFNat) (zero : motive 0) (succ : (x : ZFNat) → motive x → motive x.succ) : motive n

The recursion principle for natural numbers. This recursor allows inductive definitions over natural numbers to be defined in a more natural way.

Equations

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

theorem ZFSet.ZFNat.induction_is_rec_into_Prop {motive : ZFNat → Prop} : ⋯ = ⋯

The induction principle of ZFNat is a universe-specialized version of the recursion principle.

theorem ZFSet.ZFNat.rec_zero {motive : ZFNat → Sort u} (zero : motive 0) (succ : (x : ZFNat) → motive x → motive x.succ) : rec 0 zero succ = zero

theorem ZFSet.ZFNat.rec_succ {motive : ZFNat → Sort u} (n : ZFNat) (zero : motive 0) (succ' : (x : ZFNat) → motive x → motive x.succ) : rec n.succ zero succ' = succ' n (rec n zero succ')

@[reducible, inline]

noncomputable abbrev ZFSet.ZFNat.pred' (m : ZFNat) : ZFNat

The predecessor function pred' on natural numbers, defined inductively. This definition is equivalent to pred, as proven by pred'_eq_pred.

Equations

• m.pred' = ZFSet.ZFNat.rec m 0 fun (x x_1 : ZFSet.ZFNat) => x

theorem ZFSet.ZFNat.pred'_eq_pred : pred = ZFNat.pred'

The definitions of pred and pred' are equivalent.

Arithmetic

theorem ZFSet.ZFNat.zero_lt_succ {n : ZFNat} : 0 < n.succ

theorem ZFSet.ZFNat.pos_of_ne_zero {n : ZFNat} : 0 ≠ n → 0 < n

@[instance_reducible]

instance ZFSet.ZFNat.instPreorder : Preorder ZFNat

Equations

• ZFSet.ZFNat.instPreorder = { toLE := ZFSet.ZFNat.natLe, toLT := ZFSet.ZFNat.natLt, le_refl := ZFSet.ZFNat.instPreorder._proof_1, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

@[instance_reducible]

noncomputable instance ZFSet.ZFNat.instLinearOrder : LinearOrder ZFNat

Equations

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

instance ZFSet.ZFNat.instIsStrictTotalOrderLt : IsStrictTotalOrder ZFNat fun (x1 x2 : ZFNat) => x1 < x2

@[reducible, inline]

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

The addition function on natural numbers, defined inductively.

Equations

• n.add m = ZFSet.ZFNat.rec n m fun (x : ZFSet.ZFNat) => ZFSet.ZFNat.succ

@[instance_reducible]

noncomputable instance ZFSet.ZFNat.addInst : Add ZFNat

Equations

• ZFSet.ZFNat.addInst = { add := ZFSet.ZFNat.add }

theorem ZFSet.ZFNat.addInst_eq {n m : ZFNat} : n + m = n.add m

theorem ZFSet.ZFNat.add_one_eq_succ {n : ZFNat} : n + 1 = n.succ

theorem ZFSet.ZFNat.add_one_eq_succ' {n : ZFNat} : 1 + n = n.succ

theorem ZFSet.ZFNat.add_zero {n : ZFNat} : n + 0 = n

theorem ZFSet.ZFNat.zero_add {n : ZFNat} : 0 + n = n

theorem ZFSet.ZFNat.add_succ {n m : ZFNat} : n.succ + m = (n + m).succ

theorem ZFSet.ZFNat.succ_add {n m : ZFNat} : (n + m).succ = n + m.succ

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

@[simp]

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

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

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

theorem ZFSet.ZFNat.add_left_cancel {n m k : ZFNat} : n + m = n + k ↔ m = k

theorem ZFSet.ZFNat.add_right_cancel {n m k : ZFNat} : n + m = k + m ↔ n = k

theorem ZFSet.ZFNat.eq_zero_of_add_eq_zero {n m : ZFNat} : n + m = 0 → n = 0 ∧ m = 0

theorem ZFSet.ZFNat.eq_zero_of_add_eq_zero_left {n m : ZFNat} (h : n + m = 0) : m = 0

@[simp]

theorem ZFSet.ZFNat.add_left_eq_self {a b : ZFNat} : a + b = b ↔ a = 0

theorem ZFSet.ZFNat.add_right_eq_self {a b : ZFNat} : a + b = a ↔ b = 0

theorem ZFSet.ZFNat.self_eq_add_right {a b : ZFNat} : a = a + b ↔ b = 0

@[simp]

theorem ZFSet.ZFNat.self_eq_add_left {a b : ZFNat} : a = b + a ↔ b = 0

theorem ZFSet.ZFNat.lt_of_succ_le {n m : ZFNat} (h : n.succ ≤ m) : n < m

theorem ZFSet.ZFNat.succ_le_of_lt {n m : ZFNat} (h : n < m) : n.succ ≤ m

theorem ZFSet.ZFNat.le.dest {n m : ZFNat} : n ≤ m → ∃ (k : ZFNat), n + k = m

theorem ZFSet.ZFNat.le_succ_of_le {n m : ZFNat} (h : n ≤ m) : n ≤ m.succ

@[simp]

theorem ZFSet.ZFNat.le_add_right (n k : ZFNat) : n ≤ n + k

@[simp]

theorem ZFSet.ZFNat.le_add_left (n m : ZFNat) : n ≤ m + n

theorem ZFSet.ZFNat.le.intro {n m k : ZFNat} (h : n + k = m) : n ≤ m

theorem ZFSet.ZFNat.zero_le {n : ZFNat} : 0 ≤ n

theorem ZFSet.ZFNat.le_of_add_le_add_left {a b c : ZFNat} (h : a + b ≤ a + c) : b ≤ c

theorem ZFSet.ZFNat.add_le_add_left {n m : ZFNat} (h : n ≤ m) (k : ZFNat) : k + n ≤ k + m

@[simp]

theorem ZFSet.ZFNat.add_le_add_iff_left {n m k : ZFNat} : n + m ≤ n + k ↔ m ≤ k

theorem ZFSet.ZFNat.lt_of_add_lt_add_right {n m k : ZFNat} : k + n < m + n → k < m

theorem ZFSet.ZFNat.add_lt_add_left {n m : ZFNat} (h : n < m) (k : ZFNat) : k + n < k + m

theorem ZFSet.ZFNat.add_lt_add_right {n m : ZFNat} (h : n < m) (k : ZFNat) : n + k < m + k

theorem ZFSet.ZFNat.lt_add_of_pos_right {n k : ZFNat} (h : 0 < k) : n < n + k

theorem ZFSet.ZFNat.lt_of_add_lt_add_left {n m k : ZFNat} : n + k < n + m → k < m

@[simp]

theorem ZFSet.ZFNat.add_lt_add_iff_left {k n m : ZFNat} : k + n < k + m ↔ n < m

@[simp]

theorem ZFSet.ZFNat.add_lt_add_iff_right {k n m : ZFNat} : n + k < m + k ↔ n < m

theorem ZFSet.ZFNat.add_le_add_right {n m : ZFNat} (h : n ≤ m) (k : ZFNat) : n + k ≤ m + k

theorem ZFSet.ZFNat.add_lt_add_of_le_of_lt {a b c d : ZFNat} (hle : a ≤ b) (hlt : c < d) : a + c < b + d

theorem ZFSet.ZFNat.add_lt_add_of_lt_of_le {a b c d : ZFNat} (hlt : a < b) (hle : c ≤ d) : a + c < b + d

theorem ZFSet.ZFNat.lt_add_of_pos_left {k n : ZFNat} : 0 < k → n < k + n

theorem ZFSet.ZFNat.pos_of_lt_add_right {n k : ZFNat} (h : n < n + k) : 0 < k

theorem ZFSet.ZFNat.pos_of_lt_add_left {n k : ZFNat} : n < k + n → 0 < k

@[simp]

theorem ZFSet.ZFNat.lt_add_right_iff_pos {n k : ZFNat} : n < n + k ↔ 0 < k

@[simp]

theorem ZFSet.ZFNat.lt_add_left_iff_pos {n k : ZFNat} : n < k + n ↔ 0 < k

theorem ZFSet.ZFNat.add_pos_left {m : ZFNat} (h : 0 < m) (n : ZFNat) : 0 < m + n

theorem ZFSet.ZFNat.add_pos_right {n : ZFNat} (m : ZFNat) (h : 0 < n) : 0 < m + n

theorem ZFSet.ZFNat.pred_le_pred {n m : ZFNat} : n ≤ m → n.pred ≤ m.pred

theorem ZFSet.ZFNat.le_of_succ_le_succ {n m : ZFNat} : n.succ ≤ m.succ → n ≤ m

theorem ZFSet.ZFNat.lt_of_succ_lt_succ {n m : ZFNat} : n.succ < m.succ → n < m

theorem ZFSet.ZFNat.add_self_ne_one {n : ZFNat} : n + n ≠ 1

@[reducible, inline]

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

Natural-number subtraction in the ZF natural model.

Equations

• n.sub m = ZFSet.ZFNat.rec m n fun (x : ZFSet.ZFNat) => ZFSet.ZFNat.pred

@[instance_reducible]

noncomputable instance ZFSet.ZFNat.subInst : Sub ZFNat

Imported ZFLean declaration.

Equations

• ZFSet.ZFNat.subInst = { sub := ZFSet.ZFNat.sub }

theorem ZFSet.ZFNat.subInst_eq {n m : ZFNat} : n - m = n.sub m

theorem ZFSet.ZFNat.sub_zero {n : ZFNat} : n - 0 = n

theorem ZFSet.ZFNat.sub_one_eq_pred {n : ZFNat} : n - 1 = n.pred

theorem ZFSet.ZFNat.succ_mono {n m : ZFNat} : n < m ↔ n.succ < m.succ

theorem ZFSet.ZFNat.sub_succ (n m : ZFNat) : n - m.succ = (n - m).pred

theorem ZFSet.ZFNat.zero_sub {n : ZFNat} : 0 - n = 0

theorem ZFSet.ZFNat.succ_sub_succ (n m : ZFNat) : n.succ - m.succ = n - m

theorem ZFSet.ZFNat.succ_sub_self (n : ZFNat) : n.succ - n = 1

theorem ZFSet.ZFNat.sub_self {n : ZFNat} : n - n = 0

theorem ZFSet.ZFNat.sub_add_distrib {n m k : ZFNat} : n - (m + k) = n - m - k

theorem ZFSet.ZFNat.sub_ne_zero_of_lt {a b : ZFNat} : a < b → b - a ≠ 0

theorem ZFSet.ZFNat.le_of_succ_le {n m : ZFNat} : n.succ ≤ m → n ≤ m

theorem ZFSet.ZFNat.lt_of_succ_lt {n m : ZFNat} (h : n.succ < m) : n < m

theorem ZFSet.ZFNat.le_of_lt {n m : ZFNat} : n < m → n ≤ m

theorem ZFSet.ZFNat.add_sub_of_le {a b : ZFNat} (h : a ≤ b) : a + (b - a) = b

theorem ZFSet.ZFNat.sub_one_cancel {a b : ZFNat} : 0 < a → 0 < b → a - 1 = b - 1 → a = b

theorem ZFSet.ZFNat.sub_add_cancel {n m : ZFNat} (h : m ≤ n) : n - m + m = n

theorem ZFSet.ZFNat.add_sub_add_right (n k m : ZFNat) : n + k - (m + k) = n - m

theorem ZFSet.ZFNat.add_sub_add_left (k n m : ZFNat) : k + n - (k + m) = n - m

theorem ZFSet.ZFNat.add_sub_cancel (n m : ZFNat) : n + m - m = n

theorem ZFSet.ZFNat.add_sub_cancel_left (n m : ZFNat) : n + m - n = m

theorem ZFSet.ZFNat.add_sub_assoc {m k : ZFNat} (h : k ≤ m) (n : ZFNat) : n + m - k = n + (m - k)

theorem ZFSet.ZFNat.eq_add_of_sub_eq {a b c : ZFNat} (hle : b ≤ a) (h : a - b = c) : a = c + b

theorem ZFSet.ZFNat.sub_eq_of_eq_add {a b c : ZFNat} (h : a = c + b) : a - b = c

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

theorem ZFSet.ZFNat.sub_factor {m k n : ZFNat} : k ≤ m → m ≤ n → n - m + k = n - (m - k)

theorem ZFSet.ZFNat.sub_add_comm {m n k : ZFNat} (h : m ≤ n) : n - m + k = n + k - m

theorem ZFSet.ZFNat.succ_le_succ {n m : ZFNat} : n ≤ m → n.succ ≤ m.succ

theorem ZFSet.ZFNat.succ_le_succ_iff {a b : ZFNat} : a.succ ≤ b.succ ↔ a ≤ b

theorem ZFSet.ZFNat.le_zero_imp_eq {n : ZFNat} : n ≤ 0 → n = 0

@[reducible, inline]

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

The multiplication function on natural numbers, defined inductively.

Equations

• n.mul m = ZFSet.ZFNat.rec n 0 fun (x : ZFSet.ZFNat) (x_1 : ZFSet.ZFNat) => x_1 + m

@[instance_reducible]

noncomputable instance ZFSet.ZFNat.mulInst : Mul ZFNat

Equations

• ZFSet.ZFNat.mulInst = { mul := ZFSet.ZFNat.mul }

theorem ZFSet.ZFNat.mulInst_eq {n m : ZFNat} : n * m = n.mul m

theorem ZFSet.ZFNat.mul_zero {n : ZFNat} : n * 0 = 0

theorem ZFSet.ZFNat.zero_mul {n : ZFNat} : 0 * n = 0

theorem ZFSet.ZFNat.mul_one {n : ZFNat} : n * 1 = n

theorem ZFSet.ZFNat.one_mul {n : ZFNat} : 1 * n = n

theorem ZFSet.ZFNat.mul_succ {n m : ZFNat} : (n + 1) * m = n * m + m

theorem ZFSet.ZFNat.succ_mul {n m : ZFNat} : n.succ * m = n * m + m

theorem ZFSet.ZFNat.left_distrib {n m k : ZFNat} : n * (m + k) = n * m + n * k

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

theorem ZFSet.ZFNat.succ_mul' {n m : ZFNat} : m * n.succ = m * n + m

theorem ZFSet.ZFNat.right_distrib {n m k : ZFNat} : (n + m) * k = n * k + m * k

theorem ZFSet.ZFNat.mul_assoc (n m k : ZFNat) : n * m * k = n * (m * k)

theorem ZFSet.ZFNat.mul_left_comm (n m k : ZFNat) : n * (m * k) = m * (n * k)

theorem ZFSet.ZFNat.two_mul (n : ZFNat) : (1 + 1) * n = n + n

theorem ZFSet.ZFNat.mul_two (n : ZFNat) : n * (1 + 1) = n + n

theorem ZFSet.ZFNat.sub_lt_eq_zero {n m : ZFNat} (h : n ≤ m) : n - m = 0

theorem ZFSet.ZFNat.add_lt_trans {n m p q : ZFNat} : n < m → p < q → n + p < m + q

theorem ZFSet.ZFNat.pos_mul_pos {k n : ZFNat} (h : 0 < k) : 0 < k * n → 0 < n

theorem ZFSet.ZFNat.mul_lt_mono {n m k : ZFNat} (h : 0 < k) : n < m → k * n < k * m

theorem ZFSet.ZFNat.mul_le_mono {k m n : ZFNat} : n ≤ m → k * n ≤ k * m

theorem ZFSet.ZFNat.mul_lt_cancel {k m n : ZFNat} : k * n < k * m → n < m

theorem ZFSet.ZFNat.lt_mul_iff {n m k : ZFNat} : n < m ↔ (k + 1) * n < (k + 1) * m

theorem ZFSet.ZFNat.left_distrib_mul_sub_one {n m : ZFNat} : n * (m - 1) = n * m - n

theorem ZFSet.ZFNat.left_distrib_mul_sub_aux {n m k : ZFNat} (h : k < m) : n * (m - k) = n * m - n * k

theorem ZFSet.ZFNat.sub_eq_zero_imp_le {a b : ZFNat} : a - b = 0 ↔ a ≤ b

theorem ZFSet.ZFNat.sub_eq_zero_mul {n a b : ZFNat} : a - b = 0 → n * a - n * b = 0

theorem ZFSet.ZFNat.left_distrib_mul_sub {n m k : ZFNat} : n * (m - k) = n * m - n * k

theorem ZFSet.ZFNat.right_distrib_mul_sub {n m k : ZFNat} : (m - k) * n = m * n - k * n

theorem ZFSet.ZFNat.add_eq_zero_iff {n m : ZFNat} : n + m = 0 ↔ n = 0 ∧ m = 0

theorem ZFSet.ZFNat.mul_eq_zero_iff {n m : ZFNat} : n * m = 0 ↔ n = 0 ∨ m = 0

theorem ZFSet.ZFNat.eq_le_le_iff {n m : ZFNat} : n = m ↔ n ≤ m ∧ m ≤ n

theorem ZFSet.ZFNat.mul_left_cancel_iff {n m k : ZFNat} (k_pos : k ≠ 0) : k * m = k * n ↔ m = n

theorem ZFSet.ZFNat.mul_right_cancel_iff {n m k : ZFNat} (k_pos : k ≠ 0) : m * k = n * k ↔ m = n

@[reducible, inline]

noncomputable abbrev ZFSet.ZFNat.pow (n : ZFNat) (p : ZFNat) : ZFNat

The power function on natural numbers, defined inductively.

Equations

• n.pow p = ZFSet.ZFNat.rec p 1 fun (x : ZFSet.ZFNat) (x_1 : ZFSet.ZFNat) => x_1 * n

@[instance_reducible]

noncomputable instance ZFSet.ZFNat.powInst : HomogeneousPow ZFNat

Equations

• ZFSet.ZFNat.powInst = { pow := ZFSet.ZFNat.pow }

theorem ZFSet.ZFNat.powInst_eq {n p : ZFNat} : n ^ p = n.pow p

theorem ZFSet.ZFNat.pow_zero {n : ZFNat} : n ^ 0 = 1

theorem ZFSet.ZFNat.pow_one {n : ZFNat} : n ^ 1 = n

theorem ZFSet.ZFNat.induction' {P : ZFNat → Prop} (n : ZFNat) (zero : P 0) (succ : ∀ (n : ZFNat), P n → P (n + 1)) : P n

Induction principle for ZFNat, using natural notations.

Declared as an induction eliminator.

@[reducible, inline]

abbrev ZFSet.ZFNat.nsmul : ℕ → ZFNat → ZFNat

Scalar multiplication by a Lean natural number.

Equations

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

@[instance_reducible]

noncomputable instance ZFSet.ZFNat.instSemiring : Semiring ZFNat

Imported ZFLean declaration.

Equations

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

@[instance_reducible]

noncomputable instance ZFSet.ZFNat.instCommSemiring : CommSemiring ZFNat

Equations

• ZFSet.ZFNat.instCommSemiring = { toSemiring := ZFSet.ZFNat.instSemiring, mul_comm := ZFSet.ZFNat.mul_comm }

instance ZFSet.ZFNat.instAssociativeHAdd : Std.Associative fun (x1 x2 : ZFNat) => x1 + x2

instance ZFSet.ZFNat.instCommutativeHAdd : Std.Commutative fun (x1 x2 : ZFNat) => x1 + x2

instance ZFSet.ZFNat.instAssociativeHMul : Std.Associative fun (x1 x2 : ZFNat) => x1 * x2

instance ZFSet.ZFNat.instCommutativeHMul : Std.Commutative fun (x1 x2 : ZFNat) => x1 * x2

instance ZFSet.ZFNat.instIsLeftCancelAdd : IsLeftCancelAdd ZFNat

noncomputable def ZFSet.ZFNat.toNat (n : ZFNat) : ℕ

Converts a ZF natural number to a Lean natural number.

Equations

• n.toNat = ZFSet.ZFNat.rec n 0 fun (x : ZFSet.ZFNat) => Nat.succ

noncomputable def ZFSet.ZFNat.ofNat (n : ℕ) : ZFNat

Imported ZFLean declaration.

Equations

• ZFSet.ZFNat.ofNat n = ZFSet.ZFNat.nsmul n 1

theorem ZFSet.ZFNat.toNat_is_id {n : ℕ} : (↑n).toNat = n

theorem ZFSet.Nat.is_transitive : Nat.transitive

theorem ZFSet.Nat.is_inductive : Nat.inductiveSet

Nat is an inductive set.

theorem ZFSet.ZFNat.ofNat_inj {n m : ℕ} : ↑n = ↑m ↔ n = m

theorem ZFSet.ZFNat.toNat_eq (n : ZFNat) : ↑n.toNat = n

theorem ZFSet.ZFNat.toNat_iff {n m : ZFNat} : n = m ↔ n.toNat = m.toNat

noncomputable def ZFSet.ZFNat.instEquivZFNatNat : ZFNat ≃ ℕ

The equivalence between ZF natural numbers and Lean natural numbers.

Equations

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