class OrderedSetsFields.IsOrderedSet (α : Type u_1) (lt : α → α → Prop) : Prop

Ordered set. A type α equipped with a relation lt : α → α → Prop is an ordered set if it satisfies trichotomy (for any x y, exactly one of lt x y, lt y x, or x = y holds) and transitivity (lt x y and lt y z imply lt x z).

• trichotomy (x y : α) : lt x y ∨ lt y x ∨ x = y
• transitivity (x y z : α) : lt x y → lt y z → lt x z

theorem OrderedSetsFields.bounded_above_below_iff {α : Type u_1} [Preorder α] (E : Set α) : (BddAbove E ↔ ∃ (b : α), ∀ x ∈ E, x ≤ b) ∧ (BddBelow E ↔ ∃ (c : α), ∀ x ∈ E, c ≤ x)

Bounded above and bounded below. In a preorder, a set E is bounded above iff there exists an upper bound b with x ≤ b for all x ∈ E, and bounded below iff there exists a lower bound c with c ≤ x for all x ∈ E.

def OrderedSetsFields.HasLUBProperty (α : Type u_1) [Preorder α] : Prop

Least Upper Bound (LUB) Property. A preordered type α has the LUB property if every nonempty subset E ⊆ α that is bounded above has a least upper bound (supremum) in α.

theorem OrderedSetsFields.ordered_field_axioms (F : Type u_1) [Field F] [LinearOrder F] [IsStrictOrderedRing F] : (∀ (x y z : F), x < y → x + z < y + z) ∧ ∀ (x y : F), 0 < x → 0 < y → 0 < x * y

Ordered field axioms. In an ordered field F, the order is compatible with addition (x < y implies x + z < y + z) and with multiplication (if 0 < x and 0 < y, then 0 < x * y).

theorem RealNumbers.field_axioms (F : Type u_1) [Field F] : (∀ (x y : F), x + y = y + x) ∧ (∀ (x y z : F), x + y + z = x + (y + z)) ∧ (∃ (zero : F), ∀ (x : F), zero + x = x) ∧ (∀ (x : F), ∃ (y : F), x + y = 0) ∧ (∀ (x y : F), x * y = y * x) ∧ (∀ (x y z : F), x * y * z = x * (y * z)) ∧ (∃ (one : F), ∀ (x : F), one * x = x) ∧ (∀ (x : F), x ≠ 0 → ∃ (y : F), x * y = 1) ∧ ∀ (x y z : F), (x + y) * z = x * z + y * z

Field axioms. A field F satisfies the addition axioms (A1-A5: commutativity, associativity, existence of 0, additive inverses), the multiplication axioms (M1-M5: commutativity, associativity, existence of 1, multiplicative inverses for nonzero elements), and the distributive law (D).