2. Basic Theories🔗

Definition2.1

Group: Basic theories: numbers, bunches, sets, and the calculation style that underpins later program reasoning in LaPToP. The bunch and set material is Hehner's Sections 2.0 and 2.1; the formal counterpart lives in the Lean module LaPToP.BasicTheories.Bunch (axioms and laws) and LaPToP.BasicTheories.Numbers (named bunches, the interval, distribution). The number laws of Section 1.1 (reference §11.3.2) are in LaPToP.BasicTheories.NumberLaws . (21)

Group member previews

Preview

Definition 2.2

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0

Used by 9

Reverse dependency previews

Preview

Definition 2.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Hehner distinguishes bunches (unordered, uncontained collections that may be used as types/domains) from sets (a bunch packaged into a single value, so that it can be an element of another collection). "All sets are elements; not all bunches are elements; that is the difference between sets and bunches."

Lean is typed, so the formalization stratifies Hehner's untyped world: a bunch of elements of type \alpha is a predicate on \alpha, i.e. a Mathlib Set α (Bunch α), and a Hehner set is a one-field structure HSet α wrapping a bunch. The book's operators translate as A, B \mapsto A \cup B, A \mathbin{\lq} B \mapsto A \cap B, A \mathbin{-\!,} B \mapsto A \setminus B, A : B \mapsto A \subseteq B, x : A \mapsto x \in A, \mathit{null} \mapsto \varnothing. Because bunches are sets in Lean, the axioms of Bunch Theory become theorems.

Lean code for Definition2.1●2 definitions

abbrevdefined in LaPToP/BasicTheories/Bunch.lean

complete

abbrev LaPToP.BasicTheories.Bunch.{u} (α : Type u) : Type u

abbrev LaPToP.BasicTheories.Bunch.{u}
  (α : Type u) : Type u

A *bunch* of elements of type `α` (aPToP §2.0), modelled as a Mathlib set.
Hehner's bunches are uncontained collections; here they are predicates on `α`,
and the bunch operators are the usual set operators.

structure(1 field)defined in LaPToP/BasicTheories/Bunch.lean

complete

structure LaPToP.BasicTheories.HSet.{u} (α : Type u) : Type u

structure LaPToP.BasicTheories.HSet.{u}
  (α : Type u) : Type u

A Hehner *set* (aPToP §2.1): a bunch packaged as a single element. The book
writes `{A}` for the set containing the bunch `A` (see `Bunch.pack`) and `~S`
for the contents of the set `S` (see `HSet.contents`).

Fields

contents : LaPToP.BasicTheories.Bunch α

`~S`, the contents of the set `S`.

Definition2.2

Group member previews

Preview

Definition 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1

Used by 7

Reverse dependency previews

Preview

Theorem 2.3

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

The empty bunch \mathit{null}, the elementary bunch of a single element x (written just x in the book, {x} in Lean), and the size {\rm c\llap{/}}A of a bunch. Size takes values in the extended naturals so that {\rm c\llap{/}}\,\mathit{nat} = \infty as in the book. These are the primitives used by Definition 2.1.

Lean code for Definition2.2●3 definitions

abbrevdefined in LaPToP/BasicTheories/Bunch.lean

complete

abbrev LaPToP.BasicTheories.Bunch.null.{u} {α : Type u} :
  LaPToP.BasicTheories.Bunch α

abbrev LaPToP.BasicTheories.Bunch.null.{u}
  {α : Type u} :
  LaPToP.BasicTheories.Bunch α

`null`, the empty bunch (aPToP §2.0).

abbrevdefined in LaPToP/BasicTheories/Bunch.lean

complete

abbrev LaPToP.BasicTheories.Bunch.elem.{u} {α : Type u} (x : α) :
  LaPToP.BasicTheories.Bunch α

abbrev LaPToP.BasicTheories.Bunch.elem.{u}
  {α : Type u} (x : α) :
  LaPToP.BasicTheories.Bunch α

The elementary bunch consisting of the single element `x`. Hehner writes it
just `x`; in the typed model it is the singleton `{x}`.

abbrevdefined in LaPToP/BasicTheories/Bunch.lean

complete

abbrev LaPToP.BasicTheories.Bunch.size.{u} {α : Type u}
  (A : LaPToP.BasicTheories.Bunch α) : ℕ∞

abbrev LaPToP.BasicTheories.Bunch.size.{u}
  {α : Type u}
  (A : LaPToP.BasicTheories.Bunch α) : ℕ∞

`¢A`, the size (cardinality) of a bunch, valued in the extended naturals so
that `¢nat = ∞` as in the book.

Theorem2.3

Group member previews

Preview

Definition 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 1✓L∃∀N

EffortsmallTagsbasicbunchhehner-2.0

For elements x, y and bunches A, B: x : y = (x = y) (elementary), x : A, B = x : A \lor x : B (union), x : A \mathbin{\lq} B = x : A \land x : B (intersection), x : A \mathbin{-\!,} B = x : A \land \neg x : B (removal). In the typed model the elementary axiom reads \{x\} \subseteq \{y\} \iff x = y, and a bridging lemma identifies \{x\} \subseteq A with x \in A. Uses Definition 2.2.

Lean code for Theorem2.3●5 theorems

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.elem_subset_elem.{u} {α : Type u} (x y : α) :
  LaPToP.BasicTheories.Bunch.elem x ⊆
      LaPToP.BasicTheories.Bunch.elem y ↔
    x = y

theorem LaPToP.BasicTheories.Bunch.elem_subset_elem.{u}
  {α : Type u} (x y : α) :
  LaPToP.BasicTheories.Bunch.elem x ⊆
      LaPToP.BasicTheories.Bunch.elem y ↔
    x = y

`x: y = x=y` (elementary).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.elem_subset_iff.{u} {α : Type u} (x : α)
  (A : LaPToP.BasicTheories.Bunch α) :
  LaPToP.BasicTheories.Bunch.elem x ⊆ A ↔ x ∈ A

theorem LaPToP.BasicTheories.Bunch.elem_subset_iff.{u}
  {α : Type u} (x : α)
  (A : LaPToP.BasicTheories.Bunch α) :
  LaPToP.BasicTheories.Bunch.elem x ⊆ A ↔
    x ∈ A

An element is in a bunch iff its elementary bunch is included in it. This
bridges the two readings of Hehner's `:`.

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.mem_union.{u} {α : Type u} (x : α)
  (A B : LaPToP.BasicTheories.Bunch α) : x ∈ A ∪ B ↔ x ∈ A ∨ x ∈ B

theorem LaPToP.BasicTheories.Bunch.mem_union.{u}
  {α : Type u} (x : α)
  (A B : LaPToP.BasicTheories.Bunch α) :
  x ∈ A ∪ B ↔ x ∈ A ∨ x ∈ B

`x: A, B = x: A ∨ x: B` (union).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.mem_inter.{u} {α : Type u} (x : α)
  (A B : LaPToP.BasicTheories.Bunch α) : x ∈ A ∩ B ↔ x ∈ A ∧ x ∈ B

theorem LaPToP.BasicTheories.Bunch.mem_inter.{u}
  {α : Type u} (x : α)
  (A B : LaPToP.BasicTheories.Bunch α) :
  x ∈ A ∩ B ↔ x ∈ A ∧ x ∈ B

`x: A‘B = x: A ∧ x: B` (intersection).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.mem_remove.{u} {α : Type u} (x : α)
  (A B : LaPToP.BasicTheories.Bunch α) : x ∈ A \ B ↔ x ∈ A ∧ x ∉ B

theorem LaPToP.BasicTheories.Bunch.mem_remove.{u}
  {α : Type u} (x : α)
  (A B : LaPToP.BasicTheories.Bunch α) :
  x ∈ A \ B ↔ x ∈ A ∧ x ∉ B

`x: A–, B = x: A ∧ ¬ x: B` (removal).

Proof for Theorem 2.3

uses 0

Each is the corresponding Mathlib membership lemma for Set.

Theorem2.4

Group member previews

Preview

Definition 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 2.8

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

EffortsmallTagsbasicbunchhehner-2.0

For bunches A, B, C: union and intersection are idempotent, symmetric and associative; removal satisfies A \mathbin{-\!,} (B, C) = (A \mathbin{-\!,} B) \mathbin{-\!,} C = (A \mathbin{-\!,} B) \mathbin{\lq} (A \mathbin{-\!,} C) (union removal) and A \mathbin{\lq} (B \mathbin{-\!,} C) = (A \mathbin{\lq} B) \mathbin{-\!,} C = B \mathbin{\lq} (A \mathbin{-\!,} C) (intersection removal); and A, (B \mathbin{\lq} C) = (A, B) \mathbin{\lq} (A, C), A \mathbin{\lq} (B, C) = (A \mathbin{\lq} B), (A \mathbin{\lq} C) (distributivity). Uses Definition 2.1.

Lean code for Theorem2.4●12 theorems

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.union_self.{u} {α : Type u}
  (A : LaPToP.BasicTheories.Bunch α) : A ∪ A = A

theorem LaPToP.BasicTheories.Bunch.union_self.{u}
  {α : Type u}
  (A : LaPToP.BasicTheories.Bunch α) :
  A ∪ A = A

`A, A = A` (idempotence).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.union_comm.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) : A ∪ B = B ∪ A

theorem LaPToP.BasicTheories.Bunch.union_comm.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) :
  A ∪ B = B ∪ A

`A, B = B, A` (symmetry).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.union_assoc.{u} {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) : A ∪ (B ∪ C) = A ∪ B ∪ C

theorem LaPToP.BasicTheories.Bunch.union_assoc.{u}
  {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) :
  A ∪ (B ∪ C) = A ∪ B ∪ C

`A, (B, C) = (A, B), C` (associativity).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.inter_self.{u} {α : Type u}
  (A : LaPToP.BasicTheories.Bunch α) : A ∩ A = A

theorem LaPToP.BasicTheories.Bunch.inter_self.{u}
  {α : Type u}
  (A : LaPToP.BasicTheories.Bunch α) :
  A ∩ A = A

`A‘A = A` (idempotence).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.inter_comm.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) : A ∩ B = B ∩ A

theorem LaPToP.BasicTheories.Bunch.inter_comm.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) :
  A ∩ B = B ∩ A

`A‘B = B‘A` (symmetry).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.inter_assoc.{u} {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) : A ∩ (B ∩ C) = A ∩ B ∩ C

theorem LaPToP.BasicTheories.Bunch.inter_assoc.{u}
  {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) :
  A ∩ (B ∩ C) = A ∩ B ∩ C

`A‘(B‘C) = (A‘B)‘C` (associativity).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.remove_union.{u} {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) : A \ (B ∪ C) = (A \ B) \ C

theorem LaPToP.BasicTheories.Bunch.remove_union.{u}
  {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) :
  A \ (B ∪ C) = (A \ B) \ C

`A–, (B, C) = (A–, B)–, C` (union removal, first equation).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.remove_remove.{u} {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) : (A \ B) \ C = A \ B ∩ (A \ C)

theorem LaPToP.BasicTheories.Bunch.remove_remove.{u}
  {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) :
  (A \ B) \ C = A \ B ∩ (A \ C)

`(A–, B)–, C = (A–, B)‘(A–, C)` (union removal, second equation).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.inter_remove.{u} {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) : A ∩ (B \ C) = (A ∩ B) \ C

theorem LaPToP.BasicTheories.Bunch.inter_remove.{u}
  {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) :
  A ∩ (B \ C) = (A ∩ B) \ C

`A‘(B–, C) = (A‘B)–, C` (intersection removal, first equation).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.inter_remove_comm.{u} {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) : (A ∩ B) \ C = B ∩ (A \ C)

theorem LaPToP.BasicTheories.Bunch.inter_remove_comm.{u}
  {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) :
  (A ∩ B) \ C = B ∩ (A \ C)

`(A‘B)–, C = B‘(A–, C)` (intersection removal, second equation).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.union_inter_distrib.{u} {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) : A ∪ B ∩ C = (A ∪ B) ∩ (A ∪ C)

theorem LaPToP.BasicTheories.Bunch.union_inter_distrib.{u}
  {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) :
  A ∪ B ∩ C = (A ∪ B) ∩ (A ∪ C)

`A, (B‘C) = (A, B)‘(A, C)` (distributivity).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.inter_union_distrib.{u} {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) : A ∩ (B ∪ C) = A ∩ B ∪ A ∩ C

theorem LaPToP.BasicTheories.Bunch.inter_union_distrib.{u}
  {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) :
  A ∩ (B ∪ C) = A ∩ B ∪ A ∩ C

`A‘(B, C) = (A‘B), (A‘C)` (distributivity).

Proof for Theorem 2.4

uses 0

Lattice and set-difference identities for Set; the two removal laws without a direct Mathlib name are settled by extensionality and propositional reasoning.

Theorem2.5

Group member previews

Preview

Definition 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1

Used by 3

Reverse dependency previews

Preview

Theorem 2.8

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

EffortsmallTagsbasicbunchhehner-2.0

For bunches A, B, C: A : B \mathbin{\lq} C = A : B \land A : C (distributivity), A, B : C = A : C \land B : C (antidistributivity), A : A, B (generalization), A \mathbin{\lq} B : A (specialization), A : A (reflexivity), A : B \land B : A = (A = B) (antisymmetry), A : B \land B : C \Rightarrow A : C (transitivity), and A :: B = B : A (mirror). Uses Definition 2.1.

Lean code for Theorem2.5●8 theorems

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.subset_inter_iff.{u} {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) : A ⊆ B ∩ C ↔ A ⊆ B ∧ A ⊆ C

theorem LaPToP.BasicTheories.Bunch.subset_inter_iff.{u}
  {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) :
  A ⊆ B ∩ C ↔ A ⊆ B ∧ A ⊆ C

`A: B‘C = A: B ∧ A: C` (distributivity).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.union_subset_iff.{u} {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) : A ∪ B ⊆ C ↔ A ⊆ C ∧ B ⊆ C

theorem LaPToP.BasicTheories.Bunch.union_subset_iff.{u}
  {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) :
  A ∪ B ⊆ C ↔ A ⊆ C ∧ B ⊆ C

`A, B: C = A: C ∧ B: C` (antidistributivity).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.subset_union.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) : A ⊆ A ∪ B

theorem LaPToP.BasicTheories.Bunch.subset_union.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) :
  A ⊆ A ∪ B

`A: A, B` (generalization).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.inter_subset.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) : A ∩ B ⊆ A

theorem LaPToP.BasicTheories.Bunch.inter_subset.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) :
  A ∩ B ⊆ A

`A‘B: A` (specialization).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.subset_refl.{u} {α : Type u}
  (A : LaPToP.BasicTheories.Bunch α) : A ⊆ A

theorem LaPToP.BasicTheories.Bunch.subset_refl.{u}
  {α : Type u}
  (A : LaPToP.BasicTheories.Bunch α) :
  A ⊆ A

`A: A` (reflexivity).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.subset_antisymm_iff.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) : A ⊆ B ∧ B ⊆ A ↔ A = B

theorem LaPToP.BasicTheories.Bunch.subset_antisymm_iff.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) :
  A ⊆ B ∧ B ⊆ A ↔ A = B

`A: B ∧ B: A = A=B` (antisymmetry).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.subset_trans.{u} {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) : A ⊆ B ∧ B ⊆ C → A ⊆ C

theorem LaPToP.BasicTheories.Bunch.subset_trans.{u}
  {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) :
  A ⊆ B ∧ B ⊆ C → A ⊆ C

`A: B ∧ B: C ⇒ A: C` (transitivity).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.superset_iff.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) : A ⊇ B ↔ B ⊆ A

theorem LaPToP.BasicTheories.Bunch.superset_iff.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) :
  A ⊇ B ↔ B ⊆ A

`A:: B = B: A` (mirror).

Proof for Theorem 2.5

uses 0

Inclusion is Set subset, a partial order with the lattice structure of union and intersection; each law is the matching Mathlib fact.

Theorem2.6

Group member previews

Preview

Definition 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1

Used by 3

Reverse dependency previews

Preview

Theorem 2.7

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

EffortsmallTagsbasicbunchhehner-2.0

For an element x and bunches A, B: {\rm c\llap{/}}x = 1, {\rm c\llap{/}}(A, B) + {\rm c\llap{/}}(A \mathbin{\lq} B) = {\rm c\llap{/}}A + {\rm c\llap{/}}B, \neg x : A = ({\rm c\llap{/}}(A \mathbin{\lq} x) = 0), and A : B \Rightarrow {\rm c\llap{/}}A \le {\rm c\llap{/}}B. Uses Definition 2.2.

Lean code for Theorem2.6●4 theorems

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.size_elem.{u} {α : Type u} (x : α) :
  (LaPToP.BasicTheories.Bunch.elem x).size = 1

theorem LaPToP.BasicTheories.Bunch.size_elem.{u}
  {α : Type u} (x : α) :
  (LaPToP.BasicTheories.Bunch.elem
        x).size =
    1

`¢x = 1` (size).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.size_union_add_size_inter.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) :
  (A ∪ B).size + (A ∩ B).size = A.size + B.size

theorem LaPToP.BasicTheories.Bunch.size_union_add_size_inter.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) :
  (A ∪ B).size + (A ∩ B).size =
    A.size + B.size

`¢(A, B) + ¢(A‘B) = ¢A + ¢B` (size).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.not_mem_iff_size_inter_elem.{u} {α : Type u}
  (x : α) (A : LaPToP.BasicTheories.Bunch α) :
  x ∉ A ↔ (A ∩ LaPToP.BasicTheories.Bunch.elem x).size = 0

theorem LaPToP.BasicTheories.Bunch.not_mem_iff_size_inter_elem.{u}
  {α : Type u} (x : α)
  (A : LaPToP.BasicTheories.Bunch α) :
  x ∉ A ↔
    (A ∩
          LaPToP.BasicTheories.Bunch.elem
            x).size =
      0

`¬ x: A = ¢(A‘x) = 0` (size).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.size_le_size.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) : A ⊆ B → A.size ≤ B.size

theorem LaPToP.BasicTheories.Bunch.size_le_size.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) :
  A ⊆ B → A.size ≤ B.size

`A: B ⇒ ¢A ≤ ¢B` (size).

Proof for Theorem 2.6

uses 0

Size is Mathlib's Set.encard, valued in \mathbb{N}_\infty; the laws are encard_singleton, encard_union_add_encard_inter, encard_eq_zero, and monotonicity of encard. No finiteness hypotheses are needed.

Theorem2.7

Group member previews

Preview

Definition 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Definition 2.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

EffortsmallTagsbasicbunchhehner-2.0

The empty bunch is defined in the book by \mathit{null} : A and {\rm c\llap{/}}A = 0 = (A = \mathit{null}), giving A, \mathit{null} = A (identity), A \mathbin{\lq} \mathit{null} = \mathit{null} (base), and {\rm c\llap{/}}\,\mathit{null} = 0 (size). Uses Definition 2.2 and Theorem 2.6.

Lean code for Theorem2.7●5 theorems

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.null_subset.{u} {α : Type u}
  (A : LaPToP.BasicTheories.Bunch α) :
  LaPToP.BasicTheories.Bunch.null ⊆ A

theorem LaPToP.BasicTheories.Bunch.null_subset.{u}
  {α : Type u}
  (A : LaPToP.BasicTheories.Bunch α) :
  LaPToP.BasicTheories.Bunch.null ⊆ A

`null: A`.

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.size_eq_zero_iff.{u} {α : Type u}
  (A : LaPToP.BasicTheories.Bunch α) :
  A.size = 0 ↔ A = LaPToP.BasicTheories.Bunch.null

theorem LaPToP.BasicTheories.Bunch.size_eq_zero_iff.{u}
  {α : Type u}
  (A : LaPToP.BasicTheories.Bunch α) :
  A.size = 0 ↔
    A = LaPToP.BasicTheories.Bunch.null

`¢A = 0 = A = null`.

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.union_null.{u} {α : Type u}
  (A : LaPToP.BasicTheories.Bunch α) :
  A ∪ LaPToP.BasicTheories.Bunch.null = A

theorem LaPToP.BasicTheories.Bunch.union_null.{u}
  {α : Type u}
  (A : LaPToP.BasicTheories.Bunch α) :
  A ∪ LaPToP.BasicTheories.Bunch.null = A

`A, null = A` (identity).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.inter_null.{u} {α : Type u}
  (A : LaPToP.BasicTheories.Bunch α) :
  A ∩ LaPToP.BasicTheories.Bunch.null = LaPToP.BasicTheories.Bunch.null

theorem LaPToP.BasicTheories.Bunch.inter_null.{u}
  {α : Type u}
  (A : LaPToP.BasicTheories.Bunch α) :
  A ∩ LaPToP.BasicTheories.Bunch.null =
    LaPToP.BasicTheories.Bunch.null

`A‘null = null` (base).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.size_null.{u} {α : Type u} :
  LaPToP.BasicTheories.Bunch.null.size = 0

theorem LaPToP.BasicTheories.Bunch.size_null.{u}
  {α : Type u} :
  LaPToP.BasicTheories.Bunch.null.size = 0

`¢null = 0` (size).

Proof for Theorem 2.7

uses 0

\mathit{null} is the empty set; all five are standard Set and encard facts.

Theorem2.8

Group member previews

Preview

Definition 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Theorem 2.4

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

EffortsmallTagsbasicbunchhehner-2.0

Laws Hehner lists as provable from the axioms: A, (A \mathbin{\lq} B) = A and A \mathbin{\lq} (A, B) = A (absorption); A : B \Rightarrow C, A : C, B and A : B \Rightarrow C \mathbin{\lq} A : C \mathbin{\lq} B (monotonicity); A : B = (A, B = B) = (A = A \mathbin{\lq} B) (inclusion); A, (B, C) = (A, B), (A, C) and A \mathbin{\lq} (B \mathbin{\lq} C) = (A \mathbin{\lq} B) \mathbin{\lq} (A \mathbin{\lq} C) (distributivity); A : B \land C : D \Rightarrow A, C : B, D and A : B \land C : D \Rightarrow A \mathbin{\lq} C : B \mathbin{\lq} D (conflation). Uses Theorem 2.4 and Theorem 2.5.

Lean code for Theorem2.8●10 theorems

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.union_inter_self.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) : A ∪ A ∩ B = A

theorem LaPToP.BasicTheories.Bunch.union_inter_self.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) :
  A ∪ A ∩ B = A

`A, (A‘B) = A` (absorption).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.inter_union_self.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) : A ∩ (A ∪ B) = A

theorem LaPToP.BasicTheories.Bunch.inter_union_self.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) :
  A ∩ (A ∪ B) = A

`A‘(A, B) = A` (absorption).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.union_subset_union_right.{u} {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) : A ⊆ B → C ∪ A ⊆ C ∪ B

theorem LaPToP.BasicTheories.Bunch.union_subset_union_right.{u}
  {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) :
  A ⊆ B → C ∪ A ⊆ C ∪ B

`A: B ⇒ C, A: C, B` (monotonicity).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.inter_subset_inter_right.{u} {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) : A ⊆ B → C ∩ A ⊆ C ∩ B

theorem LaPToP.BasicTheories.Bunch.inter_subset_inter_right.{u}
  {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) :
  A ⊆ B → C ∩ A ⊆ C ∩ B

`A: B ⇒ C‘A: C‘B` (monotonicity).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.subset_iff_union_eq.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) : A ⊆ B ↔ A ∪ B = B

theorem LaPToP.BasicTheories.Bunch.subset_iff_union_eq.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) :
  A ⊆ B ↔ A ∪ B = B

`A: B = A, B = B` (inclusion, first equation).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.union_eq_iff_inter_eq.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) : A ∪ B = B ↔ A = A ∩ B

theorem LaPToP.BasicTheories.Bunch.union_eq_iff_inter_eq.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) :
  A ∪ B = B ↔ A = A ∩ B

`A, B = B = A = A‘B` (inclusion, second equation).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.union_union_distrib.{u} {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) : A ∪ (B ∪ C) = A ∪ B ∪ (A ∪ C)

theorem LaPToP.BasicTheories.Bunch.union_union_distrib.{u}
  {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) :
  A ∪ (B ∪ C) = A ∪ B ∪ (A ∪ C)

`A, (B, C) = (A, B), (A, C)` (distributivity).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.inter_inter_distrib.{u} {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) : A ∩ (B ∩ C) = A ∩ B ∩ (A ∩ C)

theorem LaPToP.BasicTheories.Bunch.inter_inter_distrib.{u}
  {α : Type u}
  (A B C : LaPToP.BasicTheories.Bunch α) :
  A ∩ (B ∩ C) = A ∩ B ∩ (A ∩ C)

`A‘(B‘C) = (A‘B)‘(A‘C)` (distributivity).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.union_subset_union.{u} {α : Type u}
  (A B C D : LaPToP.BasicTheories.Bunch α) :
  A ⊆ B ∧ C ⊆ D → A ∪ C ⊆ B ∪ D

theorem LaPToP.BasicTheories.Bunch.union_subset_union.{u}
  {α : Type u}
  (A B C D :
    LaPToP.BasicTheories.Bunch α) :
  A ⊆ B ∧ C ⊆ D → A ∪ C ⊆ B ∪ D

`A: B ∧ C: D ⇒ A, C: B, D` (conflation).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.Bunch.inter_subset_inter.{u} {α : Type u}
  (A B C D : LaPToP.BasicTheories.Bunch α) :
  A ⊆ B ∧ C ⊆ D → A ∩ C ⊆ B ∩ D

theorem LaPToP.BasicTheories.Bunch.inter_subset_inter.{u}
  {α : Type u}
  (A B C D :
    LaPToP.BasicTheories.Bunch α) :
  A ⊆ B ∧ C ⊆ D → A ∩ C ⊆ B ∩ D

`A: B ∧ C: D ⇒ A‘C: B‘D` (conflation).

Proof for Theorem 2.8

uses 0

In Lean these are proved directly from Mathlib's lattice lemmas rather than by calculation from the axiom nodes; the dependency edges record the book's derivation.

Definition2.9

Group member previews

Preview

Definition 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1

Used by 6

Reverse dependency previews

Preview

Theorem 2.10

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Hehner's useful bunches: \mathit{bin} = \top, \bot, \mathit{nat} = 0, 1, 2, \ldots, \mathit{int} = \ldots, -1, 0, 1, \ldots, and the extended versions \mathit{xnat} = \mathit{nat}, \infty and \mathit{xint} = -\infty, \mathit{int}, \infty. In the typed model \mathit{nat} and \mathit{int} are bunches of Lean integers (\mathit{nat} is \{n \mid 0 \le n\}), and the extended integers are XInt := WithBot (WithTop ℤ) with \bot = -\infty, \top = \infty, so \mathit{xnat} and \mathit{xint} are bunches of XInt; toXInt embeds \mathit{int} into them. Builds on Definition 2.2.

Lean code for Definition2.9●7 definitions

defdefined in LaPToP/BasicTheories/Numbers.lean

complete

def LaPToP.BasicTheories.Bunch.bin : LaPToP.BasicTheories.Bunch Bool

def LaPToP.BasicTheories.Bunch.bin :
  LaPToP.BasicTheories.Bunch Bool

`bin = ⊤, ⊥`, the binary values.

defdefined in LaPToP/BasicTheories/Numbers.lean

complete

def LaPToP.BasicTheories.Bunch.nat : LaPToP.BasicTheories.Bunch ℤ

def LaPToP.BasicTheories.Bunch.nat :
  LaPToP.BasicTheories.Bunch ℤ

`nat = 0, 1, 2, ...`, the natural numbers, as a bunch of integers.

defdefined in LaPToP/BasicTheories/Numbers.lean

complete

def LaPToP.BasicTheories.Bunch.int : LaPToP.BasicTheories.Bunch ℤ

def LaPToP.BasicTheories.Bunch.int :
  LaPToP.BasicTheories.Bunch ℤ

`int = ..., –2, –1, 0, 1, 2, ...`, the integer numbers.

abbrevdefined in LaPToP/BasicTheories/Numbers.lean

complete

abbrev LaPToP.BasicTheories.XInt : Type

abbrev LaPToP.BasicTheories.XInt : Type

The extended integers `–∞, ..., –1, 0, 1, ..., ∞` (`⊥ = –∞`, `⊤ = ∞`).

defdefined in LaPToP/BasicTheories/Numbers.lean

complete

def LaPToP.BasicTheories.Bunch.xnat :
  LaPToP.BasicTheories.Bunch LaPToP.BasicTheories.XInt

def LaPToP.BasicTheories.Bunch.xnat :
  LaPToP.BasicTheories.Bunch
    LaPToP.BasicTheories.XInt

`xnat = 0, 1, 2, ..., ∞`, the extended natural numbers.

defdefined in LaPToP/BasicTheories/Numbers.lean

complete

def LaPToP.BasicTheories.Bunch.xint :
  LaPToP.BasicTheories.Bunch LaPToP.BasicTheories.XInt

def LaPToP.BasicTheories.Bunch.xint :
  LaPToP.BasicTheories.Bunch
    LaPToP.BasicTheories.XInt

`xint = –∞, ..., –2, –1, 0, 1, 2, ..., ∞`, the extended integer numbers.

defdefined in LaPToP/BasicTheories/Numbers.lean

complete

def LaPToP.BasicTheories.Bunch.toXInt (n : ℤ) : LaPToP.BasicTheories.XInt

def LaPToP.BasicTheories.Bunch.toXInt
  (n : ℤ) : LaPToP.BasicTheories.XInt

The embedding of the integers into the extended integers.

Theorem2.10

Group member previews

Preview

Definition 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Definition 2.9

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

EffortsmallTagsbasicbunchhehner-2.0

The book's defining equations for the named bunches: \mathit{bin} = \top, \bot, \mathit{int} = \mathit{nat}, -\mathit{nat}, \mathit{xnat} = \mathit{nat}, \infty, \mathit{xint} = -\infty, \mathit{int}, \infty. Here -\mathit{nat} is pointwise negation (see Theorem 2.14), and the extended equations go through the embedding of Definition 2.9.

Lean code for Theorem2.10●4 theorems

theoremdefined in LaPToP/BasicTheories/Numbers.lean

complete

theorem LaPToP.BasicTheories.Bunch.bin_eq :
  LaPToP.BasicTheories.Bunch.bin =
    LaPToP.BasicTheories.Bunch.elem true ∪
      LaPToP.BasicTheories.Bunch.elem false

theorem LaPToP.BasicTheories.Bunch.bin_eq :
  LaPToP.BasicTheories.Bunch.bin =
    LaPToP.BasicTheories.Bunch.elem true ∪
      LaPToP.BasicTheories.Bunch.elem
        false

`bin = ⊤, ⊥` (the defining axiom).

theoremdefined in LaPToP/BasicTheories/Numbers.lean

complete

theorem LaPToP.BasicTheories.Bunch.int_eq :
  LaPToP.BasicTheories.Bunch.int =
    LaPToP.BasicTheories.Bunch.nat ∪ -LaPToP.BasicTheories.Bunch.nat

theorem LaPToP.BasicTheories.Bunch.int_eq :
  LaPToP.BasicTheories.Bunch.int =
    LaPToP.BasicTheories.Bunch.nat ∪
      -LaPToP.BasicTheories.Bunch.nat

`int = nat, –nat`.

theoremdefined in LaPToP/BasicTheories/Numbers.lean

complete

theorem LaPToP.BasicTheories.Bunch.xnat_eq :
  LaPToP.BasicTheories.Bunch.xnat =
    LaPToP.BasicTheories.Bunch.toXInt ''
        LaPToP.BasicTheories.Bunch.nat ∪
      LaPToP.BasicTheories.Bunch.elem ⊤

theorem LaPToP.BasicTheories.Bunch.xnat_eq :
  LaPToP.BasicTheories.Bunch.xnat =
    LaPToP.BasicTheories.Bunch.toXInt ''
        LaPToP.BasicTheories.Bunch.nat ∪
      LaPToP.BasicTheories.Bunch.elem ⊤

`xnat = nat, ∞`.

theoremdefined in LaPToP/BasicTheories/Numbers.lean

complete

theorem LaPToP.BasicTheories.Bunch.xint_eq :
  LaPToP.BasicTheories.Bunch.xint =
    LaPToP.BasicTheories.Bunch.elem ⊥ ∪
        LaPToP.BasicTheories.Bunch.toXInt ''
          LaPToP.BasicTheories.Bunch.int ∪
      LaPToP.BasicTheories.Bunch.elem ⊤

theorem LaPToP.BasicTheories.Bunch.xint_eq :
  LaPToP.BasicTheories.Bunch.xint =
    LaPToP.BasicTheories.Bunch.elem ⊥ ∪
        LaPToP.BasicTheories.Bunch.toXInt ''
          LaPToP.BasicTheories.Bunch.int ∪
      LaPToP.BasicTheories.Bunch.elem ⊤

`xint = –∞, int, ∞`.

Proof for Theorem 2.10

uses 0

Extensionality; the extended cases split on -\infty, a finite integer, or \infty and reduce to the finite statement by cast lemmas.

Theorem2.11

Group member previews

Preview

Definition 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Definition 2.9

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 2

Reverse dependency previews

Preview

Theorem 3.15

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

EffortsmallTagsbasicbunchhehner-2.0

The two axioms defining \mathit{nat}: 0, \mathit{nat}+1 : \mathit{nat} (construction) and 0, B+1 : B \Rightarrow \mathit{nat} : B (induction). "Construction says that 0, 1, 2, and so on, are in nat. Induction says that nothing else is in nat by saying that of all the bunches B satisfying the construction axiom, nat is the smallest." Here B + 1 is the pointwise sum B + \{1\} of Theorem 2.14, applied to Definition 2.9.

Lean code for Theorem2.11●2 theorems

theoremdefined in LaPToP/BasicTheories/Numbers.lean

complete

theorem LaPToP.BasicTheories.Bunch.nat_construction :
  LaPToP.BasicTheories.Bunch.elem 0 ∪
      (LaPToP.BasicTheories.Bunch.nat +
        LaPToP.BasicTheories.Bunch.elem 1) ⊆
    LaPToP.BasicTheories.Bunch.nat

theorem LaPToP.BasicTheories.Bunch.nat_construction :
  LaPToP.BasicTheories.Bunch.elem 0 ∪
      (LaPToP.BasicTheories.Bunch.nat +
        LaPToP.BasicTheories.Bunch.elem
          1) ⊆
    LaPToP.BasicTheories.Bunch.nat

`0, nat+1 : nat` (construction).

theoremdefined in LaPToP/BasicTheories/Numbers.lean

complete

theorem LaPToP.BasicTheories.Bunch.nat_induction
  (B : LaPToP.BasicTheories.Bunch ℤ)
  (h :
    LaPToP.BasicTheories.Bunch.elem 0 ∪
        (B + LaPToP.BasicTheories.Bunch.elem 1) ⊆
      B) :
  LaPToP.BasicTheories.Bunch.nat ⊆ B

theorem LaPToP.BasicTheories.Bunch.nat_induction
  (B : LaPToP.BasicTheories.Bunch ℤ)
  (h :
    LaPToP.BasicTheories.Bunch.elem 0 ∪
        (B +
          LaPToP.BasicTheories.Bunch.elem
            1) ⊆
      B) :
  LaPToP.BasicTheories.Bunch.nat ⊆ B

`0, B+1 : B ⇒ nat : B` (induction): `nat` is the smallest bunch satisfying
the construction axiom.

Proof for Theorem 2.11

uses 0

Construction is immediate from 0 \le n \Rightarrow 0 \le n+1. Induction unpacks the hypothesis into a base case and a successor step and applies integer induction from 0 upward (Int.leInduction).

Definition2.12

Group member previews

Preview

Definition 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1

Used by 4

Reverse dependency previews

Preview

Theorem 2.13

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

The interval x,..y ("x to y", not "x through y") for x \le y, with axiom i : x,..y = i : \mathit{xint} \land x \le i < y. The asymmetric notation is a reminder that the left end is included and the right end excluded. In Lean the bounds are integers and the interval is Set.Ico x y; it is a bunch in the sense of Definition 2.1.

Lean code for Definition2.12●1 definition

defdefined in LaPToP/BasicTheories/Numbers.lean

complete

def LaPToP.BasicTheories.Bunch.interval (x y : ℤ) :
  LaPToP.BasicTheories.Bunch ℤ

def LaPToP.BasicTheories.Bunch.interval
  (x y : ℤ) : LaPToP.BasicTheories.Bunch ℤ

`x,..y`, "`x` to `y`" (not "`x` through `y`"): the integers `i` with
`x ≤ i < y`.

Theorem2.13

Group member previews

Preview

Definition 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 3

Statement dependency previews

Preview

Definition 2.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

EffortsmallTagsbasicbunchhehner-2.0

The defining axiom i : x,..y = x \le i < y and the book's examples: 0,..3 = 0, 1, 2, 5,..5 = \mathit{null} (indeed x,..x = \mathit{null}), x,..x+1 = x, and {\rm c\llap{/}}(x,..y) = y - x. With integer bounds, 0,..\infty = \mathit{nat} becomes: \mathit{nat} is the union of the intervals 0,..y. The size law is stated with the truncated difference (y-x)_{\ge 0}, which equals y - x under the book's proviso x \le y. Uses Definition 2.12, Definition 2.2 and Definition 2.9.

Lean code for Theorem2.13●8 theorems

theoremdefined in LaPToP/BasicTheories/Numbers.lean

complete

theorem LaPToP.BasicTheories.Bunch.mem_interval (i x y : ℤ) :
  i ∈ LaPToP.BasicTheories.Bunch.interval x y ↔ x ≤ i ∧ i < y

theorem LaPToP.BasicTheories.Bunch.mem_interval
  (i x y : ℤ) :
  i ∈
      LaPToP.BasicTheories.Bunch.interval
        x y ↔
    x ≤ i ∧ i < y

`i: x,..y = i: xint ∧ x≤i<y` (the defining axiom, with integer bounds).

theoremdefined in LaPToP/BasicTheories/Numbers.lean

complete

theorem LaPToP.BasicTheories.Bunch.interval_zero_three :
  LaPToP.BasicTheories.Bunch.interval 0 3 =
    LaPToP.BasicTheories.Bunch.elem 0 ∪
        LaPToP.BasicTheories.Bunch.elem 1 ∪
      LaPToP.BasicTheories.Bunch.elem 2

theorem LaPToP.BasicTheories.Bunch.interval_zero_three :
  LaPToP.BasicTheories.Bunch.interval 0
      3 =
    LaPToP.BasicTheories.Bunch.elem 0 ∪
        LaPToP.BasicTheories.Bunch.elem
          1 ∪
      LaPToP.BasicTheories.Bunch.elem 2

`0,..3 = 0, 1, 2`.

theoremdefined in LaPToP/BasicTheories/Numbers.lean

complete

theorem LaPToP.BasicTheories.Bunch.interval_five_five :
  LaPToP.BasicTheories.Bunch.interval 5 5 =
    LaPToP.BasicTheories.Bunch.null

theorem LaPToP.BasicTheories.Bunch.interval_five_five :
  LaPToP.BasicTheories.Bunch.interval 5
      5 =
    LaPToP.BasicTheories.Bunch.null

`5,..5 = null`.

theoremdefined in LaPToP/BasicTheories/Numbers.lean

complete

theorem LaPToP.BasicTheories.Bunch.interval_self (x : ℤ) :
  LaPToP.BasicTheories.Bunch.interval x x =
    LaPToP.BasicTheories.Bunch.null

theorem LaPToP.BasicTheories.Bunch.interval_self
  (x : ℤ) :
  LaPToP.BasicTheories.Bunch.interval x
      x =
    LaPToP.BasicTheories.Bunch.null

`x,..x = null`, the general form of `5,..5 = null`.

theoremdefined in LaPToP/BasicTheories/Numbers.lean

complete

theorem LaPToP.BasicTheories.Bunch.interval_succ (x : ℤ) :
  LaPToP.BasicTheories.Bunch.interval x (x + 1) =
    LaPToP.BasicTheories.Bunch.elem x

theorem LaPToP.BasicTheories.Bunch.interval_succ
  (x : ℤ) :
  LaPToP.BasicTheories.Bunch.interval x
      (x + 1) =
    LaPToP.BasicTheories.Bunch.elem x

`x,..x+1 = x`.

theoremdefined in LaPToP/BasicTheories/Numbers.lean

complete

theorem LaPToP.BasicTheories.Bunch.size_interval (x y : ℤ) :
  (LaPToP.BasicTheories.Bunch.interval x y).size = ↑(y - x).toNat

theorem LaPToP.BasicTheories.Bunch.size_interval
  (x y : ℤ) :
  (LaPToP.BasicTheories.Bunch.interval x
        y).size =
    ↑(y - x).toNat

`¢(x,..y) = y–x`. The size is a natural number, so the difference is
truncated at `0`; for `x ≤ y` it is exactly `y – x` (see `size_interval_of_le`).

theoremdefined in LaPToP/BasicTheories/Numbers.lean

complete

theorem LaPToP.BasicTheories.Bunch.size_interval_of_le {x y : ℤ} (h : x ≤ y) :
  ∃ n, (LaPToP.BasicTheories.Bunch.interval x y).size = ↑n ∧ ↑n = y - x

theorem LaPToP.BasicTheories.Bunch.size_interval_of_le
  {x y : ℤ} (h : x ≤ y) :
  ∃ n,
    (LaPToP.BasicTheories.Bunch.interval x
            y).size =
        ↑n ∧
      ↑n = y - x

`¢(x,..y) = y–x` for `x ≤ y`, read back in the integers.

theoremdefined in LaPToP/BasicTheories/Numbers.lean

complete

theorem LaPToP.BasicTheories.Bunch.nat_eq_iUnion_interval :
  LaPToP.BasicTheories.Bunch.nat =
    ⋃ y, LaPToP.BasicTheories.Bunch.interval 0 y

theorem LaPToP.BasicTheories.Bunch.nat_eq_iUnion_interval :
  LaPToP.BasicTheories.Bunch.nat =
    ⋃ y,
      LaPToP.BasicTheories.Bunch.interval
        0 y

`0,..∞ = nat`: with integer bounds, `nat` is the union of the intervals
`0,..y`.

Proof for Theorem 2.13

uses 0

Membership is definitional; the examples are extensionality plus linear integer arithmetic; the size law is Set.encard of a finite integer interval (Int.card_Ico).

Theorem2.14

Group member previews

Preview

Definition 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Definition 2.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 4

Reverse dependency previews

Preview

Theorem 2.10

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

EffortsmallTagsbasicbunchhehner-2.0

"Other operators can be applied to bunches with the understanding that they apply to the elements of the bunch. In other words, they distribute over bunch union." The book's examples: -\mathit{null} = \mathit{null}, -(A, B) = -A, -B, A + \mathit{null} = \mathit{null} = \mathit{null} + A, and (A, B) + (C, D) = A+C, A+D, B+C, B+D. In Lean these are Mathlib's pointwise operations on sets (Set.neg, Set.add), which have exactly this meaning; an elementary bunch adds like its element, A + x = \{a + x \mid a : A\}. Uses Theorem 2.4 and Definition 2.2.

Lean code for Theorem2.14●6 theorems

theoremdefined in LaPToP/BasicTheories/Numbers.lean

complete

theorem LaPToP.BasicTheories.Bunch.neg_null.{u_1} {α : Type u_1} [Neg α] :
  -LaPToP.BasicTheories.Bunch.null = LaPToP.BasicTheories.Bunch.null

theorem LaPToP.BasicTheories.Bunch.neg_null.{u_1}
  {α : Type u_1} [Neg α] :
  -LaPToP.BasicTheories.Bunch.null =
    LaPToP.BasicTheories.Bunch.null

`–null = null`.

theoremdefined in LaPToP/BasicTheories/Numbers.lean

complete

theorem LaPToP.BasicTheories.Bunch.neg_union.{u_1} {α : Type u_1} [Neg α]
  (A B : LaPToP.BasicTheories.Bunch α) : -(A ∪ B) = -A ∪ -B

theorem LaPToP.BasicTheories.Bunch.neg_union.{u_1}
  {α : Type u_1} [Neg α]
  (A B : LaPToP.BasicTheories.Bunch α) :
  -(A ∪ B) = -A ∪ -B

`–(A, B) = –A, –B`.

theoremdefined in LaPToP/BasicTheories/Numbers.lean

complete

theorem LaPToP.BasicTheories.Bunch.add_null.{u_1} {α : Type u_1} [Add α]
  (A : LaPToP.BasicTheories.Bunch α) :
  A + LaPToP.BasicTheories.Bunch.null = LaPToP.BasicTheories.Bunch.null

theorem LaPToP.BasicTheories.Bunch.add_null.{u_1}
  {α : Type u_1} [Add α]
  (A : LaPToP.BasicTheories.Bunch α) :
  A + LaPToP.BasicTheories.Bunch.null =
    LaPToP.BasicTheories.Bunch.null

`A+null = null` (first equation).

theoremdefined in LaPToP/BasicTheories/Numbers.lean

complete

theorem LaPToP.BasicTheories.Bunch.null_add.{u_1} {α : Type u_1} [Add α]
  (A : LaPToP.BasicTheories.Bunch α) :
  LaPToP.BasicTheories.Bunch.null + A = LaPToP.BasicTheories.Bunch.null

theorem LaPToP.BasicTheories.Bunch.null_add.{u_1}
  {α : Type u_1} [Add α]
  (A : LaPToP.BasicTheories.Bunch α) :
  LaPToP.BasicTheories.Bunch.null + A =
    LaPToP.BasicTheories.Bunch.null

`null = null+A` (second equation).

theoremdefined in LaPToP/BasicTheories/Numbers.lean

complete

theorem LaPToP.BasicTheories.Bunch.union_add_union.{u_1} {α : Type u_1} [Add α]
  (A B C D : LaPToP.BasicTheories.Bunch α) :
  A ∪ B + (C ∪ D) = A + C ∪ (A + D) ∪ (B + C) ∪ (B + D)

theorem LaPToP.BasicTheories.Bunch.union_add_union.{u_1}
  {α : Type u_1} [Add α]
  (A B C D :
    LaPToP.BasicTheories.Bunch α) :
  A ∪ B + (C ∪ D) =
    A + C ∪ (A + D) ∪ (B + C) ∪ (B + D)

`(A, B)+(C, D) = A+C, A+D, B+C, B+D`.

theoremdefined in LaPToP/BasicTheories/Numbers.lean

complete

theorem LaPToP.BasicTheories.Bunch.add_elem.{u_1} {α : Type u_1} [Add α]
  (A : LaPToP.BasicTheories.Bunch α) (x : α) :
  A + LaPToP.BasicTheories.Bunch.elem x = (fun x_1 => x_1 + x) '' A

theorem LaPToP.BasicTheories.Bunch.add_elem.{u_1}
  {α : Type u_1} [Add α]
  (A : LaPToP.BasicTheories.Bunch α)
  (x : α) :
  A + LaPToP.BasicTheories.Bunch.elem x =
    (fun x_1 => x_1 + x) '' A

An elementary bunch adds like its element: `A+x = {a+x | a: A}`.

Proof for Theorem 2.14

uses 0

Pointwise-set lemmas from Mathlib (Set.union_add, Set.add_union, Set.add_empty, Set.add_singleton) and extensionality for negation.

Definition2.15

Group member previews

Preview

Definition 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 1✓L∃∀N

Set formation \{A\} packages a bunch into a set (Bunch.pack); contents \sim S unpackages it (HSet.contents); the power operator 𝒫A is the bunch of all sets whose contents are included in A; and \$S is the size of a set. The set operators \in, \subseteq, \cup, \cap are "promoted" from the bunch operators by acting on contents. Builds on Definition 2.1.

Lean code for Definition2.15●4 definitions

defdefined in LaPToP/BasicTheories/Bunch.lean

complete

def LaPToP.BasicTheories.Bunch.pack.{u} {α : Type u}
  (A : LaPToP.BasicTheories.Bunch α) : LaPToP.BasicTheories.HSet α

def LaPToP.BasicTheories.Bunch.pack.{u}
  {α : Type u}
  (A : LaPToP.BasicTheories.Bunch α) :
  LaPToP.BasicTheories.HSet α

`{A}`, the set containing the bunch `A` (aPToP §2.1).

abbrevdefined in LaPToP/BasicTheories/Bunch.lean

complete

abbrev LaPToP.BasicTheories.HSet.contents.{u} {α : Type u}
  (self : LaPToP.BasicTheories.HSet α) : LaPToP.BasicTheories.Bunch α

abbrev LaPToP.BasicTheories.HSet.contents.{u}
  {α : Type u}
  (self : LaPToP.BasicTheories.HSet α) :
  LaPToP.BasicTheories.Bunch α

`~S`, the contents of the set `S`.

defdefined in LaPToP/BasicTheories/Bunch.lean

complete

def LaPToP.BasicTheories.Bunch.power.{u} {α : Type u}
  (A : LaPToP.BasicTheories.Bunch α) :
  LaPToP.BasicTheories.Bunch (LaPToP.BasicTheories.HSet α)

def LaPToP.BasicTheories.Bunch.power.{u}
  {α : Type u}
  (A : LaPToP.BasicTheories.Bunch α) :
  LaPToP.BasicTheories.Bunch
    (LaPToP.BasicTheories.HSet α)

`𝒫A`, the power operator: all sets that contain only elements of `A`.

defdefined in LaPToP/BasicTheories/Bunch.lean

complete

def LaPToP.BasicTheories.HSet.card.{u} {α : Type u}
  (S : LaPToP.BasicTheories.HSet α) : ℕ∞

def LaPToP.BasicTheories.HSet.card.{u}
  {α : Type u}
  (S : LaPToP.BasicTheories.HSet α) : ℕ∞

`$S`, the size of a set, is the size of its contents.

Theorem2.16

Group member previews

Preview

Definition 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Theorem 2.5

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

EffortsmallTagsbasicsethehner-2.1

Hehner's Set Theory axioms, for a set S, bunches A, B and element x: \{\sim S\} = S (set formation), \sim\{A\} = A (contents), \$\{A\} = {\rm c\llap{/}}A (size), x \in \{B\} = x : B (elements), \{A\} \subseteq \{B\} = A : B (subset), \{A\} : 𝒫B = A : B (power), \{A\} \cup \{B\} = \{A, B\} (union), \{A\} \cap \{B\} = \{A \mathbin{\lq} B\} (intersection), and \{A\} = \{B\} = (A = B) (equation). The remaining axiom \{A\} \neq A (structure) is not an equation in the typed model: a set and its contents have different Lean types, which is exactly the distinction it records. Uses Definition 2.15 and Theorem 2.5.

Lean code for Theorem2.16●9 theorems

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.HSet.pack_contents.{u} {α : Type u}
  (S : LaPToP.BasicTheories.HSet α) : S.contents.pack = S

theorem LaPToP.BasicTheories.HSet.pack_contents.{u}
  {α : Type u}
  (S : LaPToP.BasicTheories.HSet α) :
  S.contents.pack = S

`{~S} = S` (set formation).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.HSet.contents_pack.{u} {α : Type u}
  (A : LaPToP.BasicTheories.Bunch α) : A.pack.contents = A

theorem LaPToP.BasicTheories.HSet.contents_pack.{u}
  {α : Type u}
  (A : LaPToP.BasicTheories.Bunch α) :
  A.pack.contents = A

`~{A} = A` (contents).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.HSet.card_pack.{u} {α : Type u}
  (A : LaPToP.BasicTheories.Bunch α) : A.pack.card = A.size

theorem LaPToP.BasicTheories.HSet.card_pack.{u}
  {α : Type u}
  (A : LaPToP.BasicTheories.Bunch α) :
  A.pack.card = A.size

`${A} = ¢A` (size, cardinality).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.HSet.mem_pack.{u} {α : Type u} (x : α)
  (B : LaPToP.BasicTheories.Bunch α) : x ∈ B.pack ↔ x ∈ B

theorem LaPToP.BasicTheories.HSet.mem_pack.{u}
  {α : Type u} (x : α)
  (B : LaPToP.BasicTheories.Bunch α) :
  x ∈ B.pack ↔ x ∈ B

`x ∈ {B} = x: B` (elements), for an element `x`.

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.HSet.pack_subset_pack.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) : A.pack ⊆ B.pack ↔ A ⊆ B

theorem LaPToP.BasicTheories.HSet.pack_subset_pack.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) :
  A.pack ⊆ B.pack ↔ A ⊆ B

`{A} ⊆ {B} = A: B` (subset).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.HSet.pack_mem_power.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) : A.pack ∈ B.power ↔ A ⊆ B

theorem LaPToP.BasicTheories.HSet.pack_mem_power.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) :
  A.pack ∈ B.power ↔ A ⊆ B

`{A}: 𝒫B = A: B` (power).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.HSet.pack_union_pack.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) : A.pack ∪ B.pack = (A ∪ B).pack

theorem LaPToP.BasicTheories.HSet.pack_union_pack.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) :
  A.pack ∪ B.pack = (A ∪ B).pack

`{A} ∪ {B} = {A, B}` (union).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.HSet.pack_inter_pack.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) : A.pack ∩ B.pack = (A ∩ B).pack

theorem LaPToP.BasicTheories.HSet.pack_inter_pack.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) :
  A.pack ∩ B.pack = (A ∩ B).pack

`{A} ∩ {B} = {A‘B}` (intersection).

theoremdefined in LaPToP/BasicTheories/Bunch.lean

complete

theorem LaPToP.BasicTheories.HSet.pack_inj.{u} {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) : A.pack = B.pack ↔ A = B

theorem LaPToP.BasicTheories.HSet.pack_inj.{u}
  {α : Type u}
  (A B : LaPToP.BasicTheories.Bunch α) :
  A.pack = B.pack ↔ A = B

`{A} = {B} = A = B` (equation).

Proof for Theorem 2.16

uses 0

Every law is definitional (rfl / Iff.rfl) once the set operators are defined on contents; injectivity of packaging is structure eta.

Definition2.17

Group member previews

Preview

Definition 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1

Used by 4

Reverse dependency previews

Preview

Theorem 2.18

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Hehner's numbers are the extended reals \mathit{xreal} = -\infty, \mathit{real}, \infty; Number Theory (Section 1.1) is "the theory of numbers as you learned it in school", with \infty and -\infty added and their laws stated under provisos such as -\infty < x < \infty. In Lean a number is Mathlib's EReal (Number), \bot = -\infty, \top = \infty, and the proviso is the predicate Number.Finite. Mathlib fixes values the book leaves unspecified (\infty + -\infty = -\infty, \infty \times 0 = 0, x / 0 = 0, 1/\infty = 0); the laws below are stated under the book's provisos, and the few laws the book states unconditionally that fail at those points carry the hypothesis excluding them. The named bunches \mathit{xnat}, \mathit{xint} of Definition 2.9 are the corresponding sub-bunches.

Lean code for Definition2.17●4 declarations

abbrevdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

abbrev LaPToP.BasicTheories.Number : Type

abbrev LaPToP.BasicTheories.Number : Type

A *number* (aPToP §1.1): an extended real, `–∞`, a real, or `∞`.

abbrevdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

abbrev LaPToP.BasicTheories.Number.Finite (x : LaPToP.BasicTheories.Number) :
  Prop

abbrev LaPToP.BasicTheories.Number.Finite
  (x : LaPToP.BasicTheories.Number) : Prop

`–∞ < x < ∞`: the book's proviso that `x` is finite.

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.Finite.exists_coe
  {x : LaPToP.BasicTheories.Number} (hx : x.Finite) : ∃ r, x = ↑r

theorem LaPToP.BasicTheories.Number.Finite.exists_coe
  {x : LaPToP.BasicTheories.Number}
  (hx : x.Finite) : ∃ r, x = ↑r

A finite number is a real number.

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.finite_coe (r : ℝ) :
  LaPToP.BasicTheories.Number.Finite ↑r

theorem LaPToP.BasicTheories.Number.finite_coe
  (r : ℝ) :
  LaPToP.BasicTheories.Number.Finite ↑r

Real numbers are finite.

Theorem2.18

Group member previews

Preview

Definition 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0✓L∃∀N

EffortsmallTagsbasicnumberhehner-11.3.2

Addition, negation and subtraction laws (reference §11.3.2): x + 0 = x, x + y = y + x, x + (y + z) = (x + y) + z; -\infty < x < \infty \Rightarrow (x + y = x + z) = (y = z) (Cancellation); -\infty < x \Rightarrow \infty + x = \infty, x < \infty \Rightarrow -\infty + x = -\infty (Absorption); -x = 0 - x, - -x = x, -(x + y) = -x + -y, -(x - y) = y - x, -x \times y = -(x \times y) = x \times -y, -x / y = -(x / y) = x / -y; x - 0 = x, x - y = x + -y, x + (y - z) = (x + y) - z, x - (y + z) = (x - y) - z; -\infty < x < \infty \Rightarrow (x - y = x - z) = (y = z), -\infty < x < \infty \Rightarrow x - x = 0; x < \infty \Rightarrow \infty - x = \infty, -\infty < x \Rightarrow -\infty - x = -\infty. The three laws involving -(y + z) or -(y - z) exclude the unspecified case \{y, z\} = \{\infty, -\infty\}, where Mathlib's model disagrees with the book. Uses Definition 2.17.

Lean code for Theorem2.18●22 theorems

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.add_zero (x : LaPToP.BasicTheories.Number) :
  x + 0 = x

theorem LaPToP.BasicTheories.Number.add_zero
  (x : LaPToP.BasicTheories.Number) :
  x + 0 = x

`x + 0 = x` (Identity).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.add_comm
  (x y : LaPToP.BasicTheories.Number) : x + y = y + x

theorem LaPToP.BasicTheories.Number.add_comm
  (x y : LaPToP.BasicTheories.Number) :
  x + y = y + x

`x + y = y + x` (Symmetry).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.add_assoc
  (x y z : LaPToP.BasicTheories.Number) : x + (y + z) = x + y + z

theorem LaPToP.BasicTheories.Number.add_assoc
  (x y z : LaPToP.BasicTheories.Number) :
  x + (y + z) = x + y + z

`x + (y + z) = (x + y) + z` (Associativity).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.add_left_cancel_iff
  (y z : LaPToP.BasicTheories.Number) {x : LaPToP.BasicTheories.Number}
  (hx : x.Finite) : x + y = x + z ↔ y = z

theorem LaPToP.BasicTheories.Number.add_left_cancel_iff
  (y z : LaPToP.BasicTheories.Number)
  {x : LaPToP.BasicTheories.Number}
  (hx : x.Finite) : x + y = x + z ↔ y = z

`–∞ < x < ∞ ⇒ (x + y = x + z = (y = z))` (Cancellation).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.top_add {x : LaPToP.BasicTheories.Number}
  (hx : ⊥ < x) : ⊤ + x = ⊤

theorem LaPToP.BasicTheories.Number.top_add
  {x : LaPToP.BasicTheories.Number}
  (hx : ⊥ < x) : ⊤ + x = ⊤

`–∞ < x ⇒ ∞ + x = ∞` (Absorption).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.bot_add {x : LaPToP.BasicTheories.Number}
  (_hx : x < ⊤) : ⊥ + x = ⊥

theorem LaPToP.BasicTheories.Number.bot_add
  {x : LaPToP.BasicTheories.Number}
  (_hx : x < ⊤) : ⊥ + x = ⊥

`x < ∞ ⇒ –∞ + x = –∞` (Absorption). Mathlib's `⊥ + x = ⊥` holds for all `x`.

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.neg_eq_zero_sub
  (x : LaPToP.BasicTheories.Number) : -x = 0 - x

theorem LaPToP.BasicTheories.Number.neg_eq_zero_sub
  (x : LaPToP.BasicTheories.Number) :
  -x = 0 - x

`–x = 0 – x` (Negation).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.neg_neg (x : LaPToP.BasicTheories.Number) :
  - -x = x

theorem LaPToP.BasicTheories.Number.neg_neg
  (x : LaPToP.BasicTheories.Number) :
  - -x = x

`– –x = x` (Self-inverse).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.neg_add {x y : LaPToP.BasicTheories.Number}
  (h₁ : x ≠ ⊥ ∨ y ≠ ⊤) (h₂ : x ≠ ⊤ ∨ y ≠ ⊥) : -(x + y) = -x + -y

theorem LaPToP.BasicTheories.Number.neg_add
  {x y : LaPToP.BasicTheories.Number}
  (h₁ : x ≠ ⊥ ∨ y ≠ ⊤)
  (h₂ : x ≠ ⊤ ∨ y ≠ ⊥) :
  -(x + y) = -x + -y

`–(x + y) = –x + –y` (Distributivity). The book states this for all
numbers; in Mathlib's model `∞ + –∞ = –∞`, so the law fails exactly when
`{x, y} = {∞, –∞}`, and that case is excluded by the hypotheses.

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.neg_sub {x y : LaPToP.BasicTheories.Number}
  (h₁ : x ≠ ⊥ ∨ y ≠ ⊥) (h₂ : x ≠ ⊤ ∨ y ≠ ⊤) : -(x - y) = y - x

theorem LaPToP.BasicTheories.Number.neg_sub
  {x y : LaPToP.BasicTheories.Number}
  (h₁ : x ≠ ⊥ ∨ y ≠ ⊥)
  (h₂ : x ≠ ⊤ ∨ y ≠ ⊤) : -(x - y) = y - x

`–(x – y) = y – x` (Antisymmetry), excluding the unspecified case
`{x, y} = {∞, –∞}` as in `neg_add`.

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.neg_mul
  (x y : LaPToP.BasicTheories.Number) : -x * y = -(x * y)

theorem LaPToP.BasicTheories.Number.neg_mul
  (x y : LaPToP.BasicTheories.Number) :
  -x * y = -(x * y)

`–x × y = –(x × y)` (Semi-distributivity).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.neg_mul_eq_mul_neg
  (x y : LaPToP.BasicTheories.Number) : -(x * y) = x * -y

theorem LaPToP.BasicTheories.Number.neg_mul_eq_mul_neg
  (x y : LaPToP.BasicTheories.Number) :
  -(x * y) = x * -y

`–(x × y) = x × –y` (Semi-distributivity).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.neg_div
  (x y : LaPToP.BasicTheories.Number) : -x / y = -(x / y)

theorem LaPToP.BasicTheories.Number.neg_div
  (x y : LaPToP.BasicTheories.Number) :
  -x / y = -(x / y)

`–x / y = –(x / y)` (Semi-distributivity).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.neg_div_eq_div_neg
  (x y : LaPToP.BasicTheories.Number) : -(x / y) = x / -y

theorem LaPToP.BasicTheories.Number.neg_div_eq_div_neg
  (x y : LaPToP.BasicTheories.Number) :
  -(x / y) = x / -y

`–(x / y) = x / –y` (Semi-distributivity).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.sub_zero (x : LaPToP.BasicTheories.Number) :
  x - 0 = x

theorem LaPToP.BasicTheories.Number.sub_zero
  (x : LaPToP.BasicTheories.Number) :
  x - 0 = x

`x – 0 = x` (Identity).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.sub_eq_add_neg
  (x y : LaPToP.BasicTheories.Number) : x - y = x + -y

theorem LaPToP.BasicTheories.Number.sub_eq_add_neg
  (x y : LaPToP.BasicTheories.Number) :
  x - y = x + -y

`x – y = x + –y` (Subtraction).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.add_sub
  (x y z : LaPToP.BasicTheories.Number) : x + (y - z) = x + y - z

theorem LaPToP.BasicTheories.Number.add_sub
  (x y z : LaPToP.BasicTheories.Number) :
  x + (y - z) = x + y - z

`x + (y – z) = (x + y) – z` (Addition-Subtraction).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.sub_add (x : LaPToP.BasicTheories.Number)
  {y z : LaPToP.BasicTheories.Number} (h₁ : y ≠ ⊥ ∨ z ≠ ⊤)
  (h₂ : y ≠ ⊤ ∨ z ≠ ⊥) : x - (y + z) = x - y - z

theorem LaPToP.BasicTheories.Number.sub_add
  (x : LaPToP.BasicTheories.Number)
  {y z : LaPToP.BasicTheories.Number}
  (h₁ : y ≠ ⊥ ∨ z ≠ ⊤)
  (h₂ : y ≠ ⊤ ∨ z ≠ ⊥) :
  x - (y + z) = x - y - z

`x – (y + z) = (x – y) – z` (Addition-Subtraction), excluding the
unspecified case `{y, z} = {∞, –∞}` as in `neg_add`.

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.sub_left_cancel_iff
  (y z : LaPToP.BasicTheories.Number) {x : LaPToP.BasicTheories.Number}
  (hx : x.Finite) : x - y = x - z ↔ y = z

theorem LaPToP.BasicTheories.Number.sub_left_cancel_iff
  (y z : LaPToP.BasicTheories.Number)
  {x : LaPToP.BasicTheories.Number}
  (hx : x.Finite) : x - y = x - z ↔ y = z

`–∞ < x < ∞ ⇒ (x – y = x – z = (y = z))` (Cancellation).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.sub_self {x : LaPToP.BasicTheories.Number}
  (hx : x.Finite) : x - x = 0

theorem LaPToP.BasicTheories.Number.sub_self
  {x : LaPToP.BasicTheories.Number}
  (hx : x.Finite) : x - x = 0

`–∞ < x < ∞ ⇒ x – x = 0` (Inverse).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.top_sub {x : LaPToP.BasicTheories.Number}
  (hx : x < ⊤) : ⊤ - x = ⊤

theorem LaPToP.BasicTheories.Number.top_sub
  {x : LaPToP.BasicTheories.Number}
  (hx : x < ⊤) : ⊤ - x = ⊤

`x < ∞ ⇒ ∞ – x = ∞` (Absorption).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.bot_sub {x : LaPToP.BasicTheories.Number}
  (_hx : ⊥ < x) : ⊥ - x = ⊥

theorem LaPToP.BasicTheories.Number.bot_sub
  {x : LaPToP.BasicTheories.Number}
  (_hx : ⊥ < x) : ⊥ - x = ⊥

`–∞ < x ⇒ –∞ – x = –∞` (Absorption).

Proof for Theorem 2.18

uses 0

Mathlib's EReal lemmas; the cancellation laws reduce a finite x to a real number and subtract it.

Theorem2.19

Group member previews

Preview

Definition 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0✓L∃∀N

EffortsmallTagsbasicnumberhehner-11.3.2

Multiplication, division and exponentiation laws (reference §11.3.2): -\infty < x < \infty \Rightarrow x \times 0 = 0, x \times 1 = x, x \times y = y \times x, x \times (y + z) = x \times y + x \times z, x \times (y \times z) = (x \times y) \times z; -\infty < x < \infty \land x \neq 0 \Rightarrow (x \times y = x \times z) = (y = z); 0 < x \Rightarrow x \times \infty = \infty, 0 < x \Rightarrow x \times -\infty = -\infty; x / 1 = x, x \neq 0 \Rightarrow 0 / x = 0, -\infty < x < \infty \land x \neq 0 \Rightarrow x / x = 1; x \times (y / z) = (x \times y) / z = (x / z) \times y = x / (z / y), (x / y) / z = x / (y \times z); -\infty < y < \infty \land y \neq 0 \Rightarrow (x / y) \times y = x; -\infty < x < \infty \Rightarrow x / \infty = 0 = x / -\infty (Annihilation); -\infty < x < \infty \Rightarrow x^0 = 1, x^1 = x. Distributivity is stated for finite x, y, z and (x/z) \times y = x/(z/y) for finite y: the book states them for all numbers, but they fail in Mathlib's model at \infty + -\infty and 1/\infty. Uses Definition 2.17.

Lean code for Theorem2.19●20 theorems

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.mul_zero {x : LaPToP.BasicTheories.Number}
  (_hx : x.Finite) : x * 0 = 0

theorem LaPToP.BasicTheories.Number.mul_zero
  {x : LaPToP.BasicTheories.Number}
  (_hx : x.Finite) : x * 0 = 0

`–∞ < x < ∞ ⇒ x × 0 = 0` (Base). Mathlib's `x * 0 = 0` holds for all `x`.

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.mul_one (x : LaPToP.BasicTheories.Number) :
  x * 1 = x

theorem LaPToP.BasicTheories.Number.mul_one
  (x : LaPToP.BasicTheories.Number) :
  x * 1 = x

`x × 1 = x` (Identity).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.mul_comm
  (x y : LaPToP.BasicTheories.Number) : x * y = y * x

theorem LaPToP.BasicTheories.Number.mul_comm
  (x y : LaPToP.BasicTheories.Number) :
  x * y = y * x

`x × y = y × x` (Symmetry).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.mul_add
  {x y z : LaPToP.BasicTheories.Number} (hx : x.Finite) (hy : y.Finite)
  (hz : z.Finite) : x * (y + z) = x * y + x * z

theorem LaPToP.BasicTheories.Number.mul_add
  {x y z : LaPToP.BasicTheories.Number}
  (hx : x.Finite) (hy : y.Finite)
  (hz : z.Finite) :
  x * (y + z) = x * y + x * z

`x × (y + z) = x × y + x × z` (Distributivity), for finite numbers. The
book states this for all numbers; in Mathlib's model it fails at the
unspecified point `∞ + –∞` (e.g. `x = –1`, `y = ∞`, `z = –∞`).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.mul_assoc
  (x y z : LaPToP.BasicTheories.Number) : x * (y * z) = x * y * z

theorem LaPToP.BasicTheories.Number.mul_assoc
  (x y z : LaPToP.BasicTheories.Number) :
  x * (y * z) = x * y * z

`x × (y × z) = (x × y) × z` (Associativity).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.mul_left_cancel_iff
  (y z : LaPToP.BasicTheories.Number) {x : LaPToP.BasicTheories.Number}
  (hx : x.Finite) (hx0 : x ≠ 0) : x * y = x * z ↔ y = z

theorem LaPToP.BasicTheories.Number.mul_left_cancel_iff
  (y z : LaPToP.BasicTheories.Number)
  {x : LaPToP.BasicTheories.Number}
  (hx : x.Finite) (hx0 : x ≠ 0) :
  x * y = x * z ↔ y = z

`–∞ < x < ∞ ∧ x ⧧ 0 ⇒ (x × y = x × z = (y = z))` (Cancellation).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.mul_top {x : LaPToP.BasicTheories.Number}
  (hx : 0 < x) : x * ⊤ = ⊤

theorem LaPToP.BasicTheories.Number.mul_top
  {x : LaPToP.BasicTheories.Number}
  (hx : 0 < x) : x * ⊤ = ⊤

`0 < x ⇒ x × ∞ = ∞` (Absorption).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.mul_bot {x : LaPToP.BasicTheories.Number}
  (hx : 0 < x) : x * ⊥ = ⊥

theorem LaPToP.BasicTheories.Number.mul_bot
  {x : LaPToP.BasicTheories.Number}
  (hx : 0 < x) : x * ⊥ = ⊥

`0 < x ⇒ x × –∞ = –∞` (Absorption).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.div_one (x : LaPToP.BasicTheories.Number) :
  x / 1 = x

theorem LaPToP.BasicTheories.Number.div_one
  (x : LaPToP.BasicTheories.Number) :
  x / 1 = x

`x / 1 = x` (Identity).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.zero_div {x : LaPToP.BasicTheories.Number}
  (_hx : x ≠ 0) : 0 / x = 0

theorem LaPToP.BasicTheories.Number.zero_div
  {x : LaPToP.BasicTheories.Number}
  (_hx : x ≠ 0) : 0 / x = 0

`x ⧧ 0 ⇒ 0 / x = 0` (Base). Mathlib's `0 / x = 0` holds for all `x`.

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.div_self {x : LaPToP.BasicTheories.Number}
  (hx : x.Finite) (hx0 : x ≠ 0) : x / x = 1

theorem LaPToP.BasicTheories.Number.div_self
  {x : LaPToP.BasicTheories.Number}
  (hx : x.Finite) (hx0 : x ≠ 0) :
  x / x = 1

`–∞ < x < ∞ ∧ x ⧧ 0 ⇒ x / x = 1` (Base).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.mul_div
  (x y z : LaPToP.BasicTheories.Number) : x * (y / z) = x * y / z

theorem LaPToP.BasicTheories.Number.mul_div
  (x y z : LaPToP.BasicTheories.Number) :
  x * (y / z) = x * y / z

`x × (y / z) = (x × y) / z` (Multiplication-Division).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.mul_div_eq_div_mul
  (x y z : LaPToP.BasicTheories.Number) : x * y / z = x / z * y

theorem LaPToP.BasicTheories.Number.mul_div_eq_div_mul
  (x y z : LaPToP.BasicTheories.Number) :
  x * y / z = x / z * y

`(x × y) / z = (x / z) × y` (Multiplication-Division).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.div_mul_eq_div_div
  (x z : LaPToP.BasicTheories.Number) {y : LaPToP.BasicTheories.Number}
  (hy : y.Finite) : x / z * y = x / (z / y)

theorem LaPToP.BasicTheories.Number.div_mul_eq_div_div
  (x z : LaPToP.BasicTheories.Number)
  {y : LaPToP.BasicTheories.Number}
  (hy : y.Finite) :
  x / z * y = x / (z / y)

`(x / z) × y = x / (z / y)` (Multiplication-Division), for finite `y`. The
book states this for all numbers; in Mathlib's model `1/∞ = 0` and `1/0 = 0`,
so it fails at `y = ±∞`.

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.div_div
  (x y z : LaPToP.BasicTheories.Number) : x / y / z = x / (y * z)

theorem LaPToP.BasicTheories.Number.div_div
  (x y z : LaPToP.BasicTheories.Number) :
  x / y / z = x / (y * z)

`(x / y) / z = x / (y × z)` (Multiplication-Division).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.div_mul_cancel
  (x : LaPToP.BasicTheories.Number) {y : LaPToP.BasicTheories.Number}
  (hy : y.Finite) (hy0 : y ≠ 0) : x / y * y = x

theorem LaPToP.BasicTheories.Number.div_mul_cancel
  (x : LaPToP.BasicTheories.Number)
  {y : LaPToP.BasicTheories.Number}
  (hy : y.Finite) (hy0 : y ≠ 0) :
  x / y * y = x

`–∞ < y < ∞ ∧ y ⧧ 0 ⇒ (x / y) × y = x` (Multiplication-Division).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.div_top {x : LaPToP.BasicTheories.Number}
  (_hx : x.Finite) : x / ⊤ = 0

theorem LaPToP.BasicTheories.Number.div_top
  {x : LaPToP.BasicTheories.Number}
  (_hx : x.Finite) : x / ⊤ = 0

`–∞ < x < ∞ ⇒ x / ∞ = 0` (Annihilation). Mathlib's `x / ⊤ = 0` holds for all `x`.

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.div_bot {x : LaPToP.BasicTheories.Number}
  (_hx : x.Finite) : x / ⊥ = 0

theorem LaPToP.BasicTheories.Number.div_bot
  {x : LaPToP.BasicTheories.Number}
  (_hx : x.Finite) : x / ⊥ = 0

`–∞ < x < ∞ ⇒ x / –∞ = 0` (Annihilation). Mathlib's `x / ⊥ = 0` holds for all `x`.

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.pow_zero {x : LaPToP.BasicTheories.Number}
  (_hx : x.Finite) : x ^ 0 = 1

theorem LaPToP.BasicTheories.Number.pow_zero
  {x : LaPToP.BasicTheories.Number}
  (_hx : x.Finite) : x ^ 0 = 1

`–∞ < x < ∞ ⇒ x^0 = 1` (Base). Mathlib's `x ^ 0 = 1` holds for all `x`.

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.pow_one (x : LaPToP.BasicTheories.Number) :
  x ^ 1 = x

theorem LaPToP.BasicTheories.Number.pow_one
  (x : LaPToP.BasicTheories.Number) :
  x ^ 1 = x

`x^1 = x` (Identity).

Proof for Theorem 2.19

uses 0

EReal is a commutative monoid with zero and a DivInvMonoid; the finite cases reduce to real arithmetic through the coercion.

Theorem2.20

Group member previews

Preview

Definition 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 1✓L∃∀N

EffortsmallTagsbasicnumberhehner-11.3.2

Order laws (reference §11.3.2): -\infty < 0 < 1 < \infty (Direction), (x < y) = (-y < -x) (Reflection), -\infty < x < \infty \Rightarrow (x + y < x + z) = (y < z) (Cancellation, Translation), 0 < x < \infty \Rightarrow (x \times y < x \times z) = (y < z) (Cancellation, Scale), x < y \lor x = y \lor x > y (Trichotomy), -\infty \le x \le \infty (Extremes), x \uparrow \infty = \infty and x \downarrow -\infty = -\infty (Base), where \uparrow/\downarrow are maximum/minimum. Uses Definition 2.17.

Lean code for Theorem2.20●9 theorems

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.direction : ⊥ < 0 ∧ 0 < 1 ∧ 1 < ⊤

theorem LaPToP.BasicTheories.Number.direction :
  ⊥ < 0 ∧ 0 < 1 ∧ 1 < ⊤

`–∞ < 0 < 1 < ∞` (Direction).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.lt_iff_neg_lt_neg
  (x y : LaPToP.BasicTheories.Number) : x < y ↔ -y < -x

theorem LaPToP.BasicTheories.Number.lt_iff_neg_lt_neg
  (x y : LaPToP.BasicTheories.Number) :
  x < y ↔ -y < -x

`x < y = –y < –x` (Reflection).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.add_lt_add_iff_left
  (y z : LaPToP.BasicTheories.Number) {x : LaPToP.BasicTheories.Number}
  (hx : x.Finite) : x + y < x + z ↔ y < z

theorem LaPToP.BasicTheories.Number.add_lt_add_iff_left
  (y z : LaPToP.BasicTheories.Number)
  {x : LaPToP.BasicTheories.Number}
  (hx : x.Finite) : x + y < x + z ↔ y < z

`–∞ < x < ∞ ⇒ (x + y < x + z = (y < z))` (Cancellation, Translation).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.coe_mul_lt_coe_mul_iff
  (y z : LaPToP.BasicTheories.Number) {r : ℝ} (hr : 0 < r) :
  ↑r * y < ↑r * z ↔ y < z

theorem LaPToP.BasicTheories.Number.coe_mul_lt_coe_mul_iff
  (y z : LaPToP.BasicTheories.Number)
  {r : ℝ} (hr : 0 < r) :
  ↑r * y < ↑r * z ↔ y < z

Multiplication by a positive real preserves strict order on either side.

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.mul_lt_mul_iff_left
  (y z : LaPToP.BasicTheories.Number) {x : LaPToP.BasicTheories.Number}
  (hx0 : 0 < x) (hx : x < ⊤) : x * y < x * z ↔ y < z

theorem LaPToP.BasicTheories.Number.mul_lt_mul_iff_left
  (y z : LaPToP.BasicTheories.Number)
  {x : LaPToP.BasicTheories.Number}
  (hx0 : 0 < x) (hx : x < ⊤) :
  x * y < x * z ↔ y < z

`0 < x < ∞ ⇒ (x × y < x × z = (y < z))` (Cancellation, Scale).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.trichotomy
  (x y : LaPToP.BasicTheories.Number) : x < y ∨ x = y ∨ x > y

theorem LaPToP.BasicTheories.Number.trichotomy
  (x y : LaPToP.BasicTheories.Number) :
  x < y ∨ x = y ∨ x > y

`x < y ∨ x = y ∨ x > y` (Trichotomy).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.extremes (x : LaPToP.BasicTheories.Number) :
  ⊥ ≤ x ∧ x ≤ ⊤

theorem LaPToP.BasicTheories.Number.extremes
  (x : LaPToP.BasicTheories.Number) :
  ⊥ ≤ x ∧ x ≤ ⊤

`–∞ ≤ x ≤ ∞` (Extremes).

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.max_top (x : LaPToP.BasicTheories.Number) :
  max x ⊤ = ⊤

theorem LaPToP.BasicTheories.Number.max_top
  (x : LaPToP.BasicTheories.Number) :
  max x ⊤ = ⊤

`x ↑ ∞ = ∞` (Base): the maximum with `∞`.

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.min_bot (x : LaPToP.BasicTheories.Number) :
  min x ⊥ = ⊥

theorem LaPToP.BasicTheories.Number.min_bot
  (x : LaPToP.BasicTheories.Number) :
  min x ⊥ = ⊥

`x ↓ –∞ = –∞` (Base): the minimum with `–∞`.

Proof for Theorem 2.20

uses 0

EReal is a complete linear order; Translation and Scale reduce a finite x to a positive real and case-split y, z over -\infty, real, \infty.

Theorem2.21

Group member previews

Preview

Definition 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 1used by 0✓L∃∀N

EffortsmallTagsbasicarithmetic

For every natural number n, adding zero on the right leaves it unchanged: n + 0 = n. A trivial arithmetic checkpoint before connecting to Definition 2.1.

Lean code for Theorem2.21●1 theorem

theoremdefined in LaPToP/BasicTheories/NumberLaws.lean

complete

theorem LaPToP.BasicTheories.Number.add_zero (x : LaPToP.BasicTheories.Number) :
  x + 0 = x

theorem LaPToP.BasicTheories.Number.add_zero
  (x : LaPToP.BasicTheories.Number) :
  x + 0 = x

`x + 0 = x` (Identity).

Proof for Theorem 2.21

uses 0

Induct on n, or use the kernel simplifier.

Lean code for Theorem2.21

theorem nat_add_zero (n : Nat) : n + 0 = n := byn:ℕ⊢ n + 0 = n
  simpAll goals completed! 🐙

Definition2.22

Group member previews

Preview

Definition 2.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 0XL∃∀N

Proofs in LaPToP are often written as calculations: chains of equalities or implications annotated with the justifying law at each step. Formal Lean proofs should preserve that readable structure where practical.