structure OrderedSet (α : Type u) : Type u

Definition 1.1.1: An ordered set is a set S with a relation < such that (i) (trichotomy) for all x y ∈ S, exactly one of x < y, x = y, or y < x holds, and (ii) (transitivity) if x < y and y < z then x < z. We write x ≤ y if x < y or x = y, and define >, ≥ analogously.

• lt : α → α → Prop
• trichotomous (x y : α) : self.lt x y ∨ x = y ∨ self.lt y x
• irrefl (x : α) : ¬self.lt x x
• trans {x y z : α} : self.lt x y → self.lt y z → self.lt x z

def OrderedSet.le {α : Type u} (S : OrderedSet α) (x y : α) : Prop

The weak order associated to an ordered set.

theorem OrderedSet.toStrictTotalOrder {α : Type u} (S : OrderedSet α) : IsStrictTotalOrder α S.lt

The axioms of an ordered set give a strict total order in mathlib's sense.

def OrderedSet.ofStrictTotalOrder {α : Type u} {lt : α → α → Prop} (h : IsStrictTotalOrder α lt) : OrderedSet α

A strict total order in mathlib yields the ordered-set structure described in Definition 1.1.1.

Definition 1.1.2: For a subset E of an ordered set S, (i) E is bounded above if there is b with x ≤ b for all x ∈ E, and such a b is an upper bound; (ii) E is bounded below if there is b with x ≥ b for all x ∈ E, and such a b is a lower bound; (iii) an upper bound b₀ is a least upper bound (supremum) if b₀ ≤ b for all upper bounds b, written sup E = b₀; (iv) a lower bound b₀ is a greatest lower bound (infimum) if b ≤ b₀ for all lower bounds b, written inf E = b₀. A set bounded above and below is called bounded.

def OrderedSet.IsUpperBound {α : Type u} (S : OrderedSet α) (E : Set α) (b : α) : Prop

An element bounding every member of E above.

def OrderedSet.IsLowerBound {α : Type u} (S : OrderedSet α) (E : Set α) (b : α) : Prop

An element bounding every member of E below.

def OrderedSet.BoundedAbove {α : Type u} (S : OrderedSet α) (E : Set α) : Prop

Existence of an upper bound for E.

def OrderedSet.BoundedBelow {α : Type u} (S : OrderedSet α) (E : Set α) : Prop

Existence of a lower bound for E.

def OrderedSet.IsLeastUpperBound {α : Type u} (S : OrderedSet α) (E : Set α) (b₀ : α) : Prop

An upper bound that is minimal among all upper bounds.

def OrderedSet.IsGreatestLowerBound {α : Type u} (S : OrderedSet α) (E : Set α) (b₀ : α) : Prop

A lower bound that is maximal among all lower bounds.

def OrderedSet.Bounded {α : Type u} (S : OrderedSet α) (E : Set α) : Prop

A set that is both bounded above and bounded below.

noncomputable def OrderedSet.supremum {α : Type u} (S : OrderedSet α) (E : Set α) (h : ∃ (b₀ : α), S.IsLeastUpperBound E b₀) : α

noncomputable def OrderedSet.infimum {α : Type u} (S : OrderedSet α) (E : Set α) (h : ∃ (b₀ : α), S.IsGreatestLowerBound E b₀) : α

theorem OrderedSet.supremum_spec {α : Type u} (S : OrderedSet α) (E : Set α) (h : ∃ (b₀ : α), S.IsLeastUpperBound E b₀) : S.IsLeastUpperBound E (S.supremum E h)

theorem OrderedSet.infimum_spec {α : Type u} (S : OrderedSet α) (E : Set α) (h : ∃ (b₀ : α), S.IsGreatestLowerBound E b₀) : S.IsGreatestLowerBound E (S.infimum E h)

def OrderedSet.LeastUpperBoundProperty {α : Type u} (S : OrderedSet α) : Prop

Definition 1.1.3: An ordered set has the least-upper-bound property if every nonempty subset that is bounded above has a least upper bound (supremum) in the set.

theorem OrderedSet.boundedAbove_iff_bddAbove {α : Type u} (S : OrderedSet α) (E : Set α) [Preorder α] (hle : ∀ (x y : α), S.le x y ↔ x ≤ y) : S.BoundedAbove E ↔ BddAbove E

theorem OrderedSet.boundedBelow_iff_bddBelow {α : Type u} (S : OrderedSet α) (E : Set α) [Preorder α] (hle : ∀ (x y : α), S.le x y ↔ x ≤ y) : S.BoundedBelow E ↔ BddBelow E

theorem OrderedSet.leastUpperBound_iff_isLUB {α : Type u} (S : OrderedSet α) (E : Set α) [Preorder α] {b₀ : α} (hle : ∀ (x y : α), S.le x y ↔ x ≤ y) : S.IsLeastUpperBound E b₀ ↔ IsLUB E b₀

theorem OrderedSet.greatestLowerBound_iff_isGLB {α : Type u} (S : OrderedSet α) (E : Set α) [Preorder α] {b₀ : α} (hle : ∀ (x y : α), S.le x y ↔ x ≤ y) : S.IsGreatestLowerBound E b₀ ↔ IsGLB E b₀

theorem OrderedSet.leastUpperBoundProperty_iff {α : Type u} (S : OrderedSet α) [Preorder α] (hle : ∀ (x y : α), S.le x y ↔ x ≤ y) : S.LeastUpperBoundProperty ↔ ∀ {E : Set α}, E.Nonempty → BddAbove E → ∃ (b₀ : α), IsLUB E b₀

theorem rat_sq_lt_two_has_no_sup : ¬∃ (q : ℚ), IsLUB {x : ℚ | x * x < 2} q

Example 1.1.4: The subset {x : ℚ | x^2 < 2} has no supremum in ℚ, so ℚ does not have the least-upper-bound property. Equivalently, there is no rational square root of 2.

theorem rational_sq_eq_two_absurd : ¬∃ (x : ℚ), x * x = 2

No rational number has square equal to 2.

structure FieldAxioms (F : Type u) [Add F] [Mul F] [Zero F] [One F] [Neg F] [Inv F] : Prop

Definition 1.1.5: A field is a set F with addition and multiplication such that (A1) if x,y ∈ F then x + y ∈ F; (A2) addition is commutative; (A3) addition is associative; (A4) there is 0 ∈ F with 0 + x = x; (A5) every x has an additive inverse -x with x + (-x) = 0; (M1) if x,y ∈ F then x * y ∈ F; (M2) multiplication is commutative; (M3) multiplication is associative; (M4) there is 1 ∈ F with 1 * x = x and 1 ≠ 0; (M5) every x ≠ 0 has a multiplicative inverse x⁻¹ with x * x⁻¹ = 1; and (D) distributivity x * (y + z) = x * y + x * z holds.

• add_comm (x y : F) : x + y = y + x
• add_assoc (x y z : F) : x + y + z = x + (y + z)
• zero_add (x : F) : 0 + x = x
• add_left_neg (x : F) : x + -x = 0
• mul_comm (x y : F) : x * y = y * x
• mul_assoc (x y z : F) : x * y * z = x * (y * z)
• one_mul (x : F) : 1 * x = x
• mul_inv_cancel {x : F} : x ≠ 0 → x * x⁻¹ = 1
• distrib (x y z : F) : x * (y + z) = x * y + x * z
• one_ne_zero : 1 ≠ 0

theorem field_axioms_of_field (F : Type u) [Field F] : FieldAxioms F

Mathlib's Field structure satisfies the axioms in Definition 1.1.5.

theorem FieldAxioms.add_zero (F : Type u) [Add F] [Mul F] [Zero F] [One F] [Neg F] [Inv F] (h : FieldAxioms F) (x : F) : x + 0 = x

From the field axioms we can derive the right identity for addition.

theorem FieldAxioms.mul_one (F : Type u) [Add F] [Mul F] [Zero F] [One F] [Neg F] [Inv F] (h : FieldAxioms F) (x : F) : x * 1 = x

From the field axioms we can derive right multiplication by 1.

theorem FieldAxioms.right_distrib (F : Type u) [Add F] [Mul F] [Zero F] [One F] [Neg F] [Inv F] (h : FieldAxioms F) (x y z : F) : (x + y) * z = x * z + y * z

From the field axioms we obtain right distributivity.

theorem FieldAxioms.mul_zero (F : Type u) [Add F] [Mul F] [Zero F] [One F] [Neg F] [Inv F] (h : FieldAxioms F) (x : F) : x * 0 = 0

From the field axioms we can show that x * 0 = 0.

theorem FieldAxioms.zero_mul (F : Type u) [Add F] [Mul F] [Zero F] [One F] [Neg F] [Inv F] (h : FieldAxioms F) (x : F) : 0 * x = 0

From the field axioms we can show that 0 * x = 0.

noncomputable def field_structure_from_axioms (F : Type u) [Add F] [Mul F] [Zero F] [One F] [Neg F] [Inv F] (h : FieldAxioms F) : Field F

Construct a mathlib Field structure from the axioms in Definition 1.1.5.

theorem field_of_field_axioms (F : Type u) [Add F] [Mul F] [Zero F] [One F] [Neg F] [Inv F] (h : FieldAxioms F) : Nonempty (Field F)

The axioms in Definition 1.1.5 recover the existence of a mathlib Field structure.

theorem field_iff_field_axioms (F : Type u) : (∃ (inst : Field F), have x := inst; FieldAxioms F) ↔ Nonempty (Field F)

The book's axioms for a field are equivalent to the existence of a mathlib Field structure using the same operations.

theorem rationals_field : Nonempty (Field ℚ)

Example 1.1.6: The rationals ℚ form a field, while the integers ℤ fail axiom (M5) because 2 has no multiplicative inverse; this is the only field axiom that does not hold for ℤ.

theorem two_mul_eq_one_int_absurd : ¬∃ (x : ℤ), 2 * x = 1

The multiplicative inverse required by (M5) for 2 : ℤ does not exist.

theorem integers_not_field : ¬IsField ℤ

The usual ring structure on the integers does not extend to a field structure.

structure OrderedFieldAxioms (F : Type u) [Field F] [LT F] : Prop

Definition 1.1.7: An ordered field is a field equipped with a strict total order such that (i) x < y implies x + z < y + z for all x y z, and (ii) 0 < x and 0 < y imply 0 < x * y. Elements with 0 < x are positive, those with x < 0 are negative, 0 < x ∨ x = 0 are nonnegative, and x < 0 ∨ x = 0 are nonpositive.

• order : IsStrictTotalOrder F fun (x1 x2 : F) => x1 < x2
• add_lt_add {x y z : F} : x < y → x + z < y + z
• mul_pos {x y : F} : 0 < x → 0 < y → 0 < x * y

def isPositive (F : Type u) [Field F] [LT F] (x : F) : Prop

An element is positive if it is greater than zero.

def isNegative (F : Type u) [Field F] [LT F] (x : F) : Prop

An element is negative if it is less than zero.

def isNonnegative (F : Type u) [Field F] [LT F] (x : F) : Prop

An element is nonnegative if it is positive or zero.

def isNonpositive (F : Type u) [Field F] [LT F] (x : F) : Prop

An element is nonpositive if it is negative or zero.

theorem orderedFieldAxioms_of_isStrictOrderedRing (F : Type u) [Field F] [LinearOrder F] [IsStrictOrderedRing F] : OrderedFieldAxioms F

Mathlib's ordered ring structure (Field together with a linear order and compatibility axioms) satisfies the ordered-field axioms in Definition 1.1.7.

theorem orderedField_iff_isStrictOrderedRing (F : Type u) [Field F] [LinearOrder F] : OrderedFieldAxioms F ↔ IsStrictOrderedRing F

The book's ordered-field axioms are equivalent to the existence of a mathlib structure using the same operations.

theorem orderedField_neg_of_pos_iff {F : Type u} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {x : F} : x > 0 ↔ -x < 0

Proposition 1.1.8: Let F be an ordered field and x y z w ∈ F. (i) If x > 0, then -x < 0 (and conversely). (ii) If x > 0 and y < z, then x * y < x * z. (iii) If x < 0 and y < z, then x * y > x * z. (iv) If x ≠ 0, then x^2 > 0. (v) If 0 < x < y, then 0 < 1 / y < 1 / x. (vi) If 0 < x < y, then x^2 < y^2. (vii) If x ≤ y and z ≤ w, then x + z ≤ y + w.

theorem orderedField_mul_lt_mul_left_of_pos {F : Type u} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {x y z : F} (hx : 0 < x) (hyz : y < z) : x * y < x * z

theorem orderedField_mul_gt_mul_left_of_neg {F : Type u} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {x y z : F} (hx : x < 0) (hyz : y < z) : x * y > x * z

theorem orderedField_sq_pos_of_ne_zero {F : Type u} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {x : F} (hx : x ≠ 0) : x ^ 2 > 0

theorem orderedField_inv_bounds_of_lt {F : Type u} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {x y : F} (hx : 0 < x) (hxy : x < y) : 0 < 1 / y ∧ 1 / y < 1 / x

theorem orderedField_sq_lt_sq_of_pos_of_lt {F : Type u} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {x y : F} (hx : 0 < x) (hxy : x < y) : x ^ 2 < y ^ 2

theorem orderedField_add_le_add {F : Type u} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {x y z w : F} (hxy : x ≤ y) (hzw : z ≤ w) : x + z ≤ y + w

theorem pos_mul_same_sign {F : Type u} [Field F] [LinearOrder F] [IsStrictOrderedRing F] {x y : F} (h : x * y > 0) : 0 < x ∧ 0 < y ∨ x < 0 ∧ y < 0

Proposition 1.1.9: In an ordered field, if x * y > 0 then either both x and y are positive or both are negative.

theorem complex_field : Nonempty (Field ℂ)

Example 1.1.10: The complex numbers ℂ = {x + iy | x y ∈ ℝ} satisfy I^2 = -1 and form a field. No ordering of ℂ can make it an ordered field: in every ordered field, -1 < 0 and squares of nonzero elements are positive, but (I : ℂ)^2 = -1.

theorem complex_I_square_pos [LinearOrder ℂ] [IsStrictOrderedRing ℂ] : 0 < Complex.I ^ 2

theorem complex_not_linearOrderedField : ¬∃ (x : LinearOrder ℂ), IsStrictOrderedRing ℂ

There is no way to equip ℂ with a linear order making it an ordered field.

theorem infimum_exists_of_bddBelow {F : Type u} [Field F] [LinearOrder F] [IsStrictOrderedRing F] (lub : ∀ {E : Set F}, E.Nonempty → BddAbove E → ∃ (b₀ : F), IsLUB E b₀) {A : Set F} (hA : A.Nonempty) (hB : BddBelow A) : ∃ (infA : F), IsGLB A infA

Proposition 1.1.11: In an ordered field with the least-upper-bound property, every nonempty subset that is bounded below has an infimum.