| Description: Define the 'greater than
or equal' predicate over the reals. Defined in
ISO 80000-2:2009(E) operation 2-7.10. It is used as a primitive in the
"NIST Digital Library of Mathematical Functions" , front
introduction,
"Common Notations and Definitions" section at
http://dlmf.nist.gov/front/introduction#Sx4.
This relation is merely
the converse of the 'less than or equal to' relation defined by df-le 10675.
We do not write this as (𝑥 ≥ 𝑦 ↔ 𝑦 ≤ 𝑥), and similarly we do
not write ` > ` as (𝑥 > 𝑦 ↔ 𝑦 < 𝑥), because these are not
definitional axioms as understood by mmj2 (those definitions will be
flagged as being "potentially non-conservative"). We could
write them
this way:
⊢
> = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ 𝑦 < 𝑥)} and
⊢
≥ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) ∧ 𝑦 ≤ 𝑥)} but
these are very complicated. This definition of ≥, and the similar
one for > (df-gt 44816), are a bit strange when you see them for
the
first time, but these definitions are much simpler for us to process and
are clearly conservative definitions. (My thanks to Mario Carneiro for
pointing out this simpler approach.) See gte-lte 44817 for a more
conventional expression of the relationship between < and >. As
a stylistic issue, set.mm prefers 'less than' instead of 'greater than' to
reduce the number of conversion steps. Thus, we discourage its use, but
include its definition so that there is a formal definition of this
symbol.
(Contributed by David A. Wheeler, 10-May-2015.)
(New usage is discouraged.) |
