Mathematical order and extrema for P3109

Finite extrema agree with the rational field's minimum and maximum. Comparisons agree with rational order, while NaN remains unordered. Magnitude ties and the preference for finite values are stated separately from rounding. The executable extrema use the same binaryTo refinement as arithmetic, so these identities describe the expression at their single projection boundary.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Arithmetic.less_finite (left right : ℚ) : less (Numerics.NumericalValue.finite left) (Numerics.NumericalValue.finite right) = true ↔ left < right

Finite strict comparison is precisely rational strict order.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Arithmetic.lessEqual_finite (left right : ℚ) : lessEqual (Numerics.NumericalValue.finite left) (Numerics.NumericalValue.finite right) = true ↔ left ≤ right

Finite non-strict comparison is precisely rational order.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Arithmetic.equal_finite (left right : ℚ) : equal (Numerics.NumericalValue.finite left) (Numerics.NumericalValue.finite right) = true ↔ left = right

Finite comparison equality is precisely equality of rational values.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Arithmetic.less_self (value : Numerics.NumericalValue ℚ) : less value value = false

No datum is strictly less than itself, even NaN.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Arithmetic.minimum_finite (left right : ℚ) : minimum (Numerics.NumericalValue.finite left) (Numerics.NumericalValue.finite right) = Numerics.NumericalValue.finite (min left right)

Finite minimum is the ordinary rational minimum.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Arithmetic.maximum_finite (left right : ℚ) : maximum (Numerics.NumericalValue.finite left) (Numerics.NumericalValue.finite right) = Numerics.NumericalValue.finite (max left right)

Finite maximum is the ordinary rational maximum.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.minimum_comm (left right : Numerics.NumericalValue ℚ) : minimum left right = minimum right left

Exact closed minimum is commutative, including NaN and infinity.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.maximum_comm (left right : Numerics.NumericalValue ℚ) : maximum left right = maximum right left

Exact closed maximum is commutative, including NaN and infinity.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Arithmetic.minimumFinite_finite_infinity (value : ℚ) (negative : Bool) : minimumFinite (Numerics.NumericalValue.finite value) (Numerics.NumericalValue.infinity negative) = Numerics.NumericalValue.finite value

A finite operand wins over either infinity in minimum-finite.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Arithmetic.maximumFinite_finite_infinity (value : ℚ) (negative : Bool) : maximumFinite (Numerics.NumericalValue.finite value) (Numerics.NumericalValue.infinity negative) = Numerics.NumericalValue.finite value

A finite operand wins over either infinity in maximum-finite.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Arithmetic.minimumNumber_nan_finite (value : ℚ) : minimumNumber nan (Numerics.NumericalValue.finite value) = Numerics.NumericalValue.finite value

The number variant ignores NaN in favor of a finite operand.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Arithmetic.maximumNumber_nan_finite (value : ℚ) : maximumNumber nan (Numerics.NumericalValue.finite value) = Numerics.NumericalValue.finite value

The number variant ignores NaN in favor of a finite operand.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.minimumMagnitude_neg_self (value : ℚ) (hvalue : 0 ≤ value) : minimumMagnitude (Numerics.NumericalValue.finite (-value)) (Numerics.NumericalValue.finite value) = Numerics.NumericalValue.finite (-value)

Equal nonnegative magnitudes are resolved toward the negative datum by minimum.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.maximumMagnitude_neg_self (value : ℚ) (hvalue : 0 ≤ value) : maximumMagnitude (Numerics.NumericalValue.finite (-value)) (Numerics.NumericalValue.finite value) = Numerics.NumericalValue.finite value

Equal nonnegative magnitudes are resolved toward the positive datum by maximum.