Users' Mathboxes Mathbox for David A. Wheeler < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-gte Structured version   Visualization version   GIF version

Definition df-gte 46095
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 10873.

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 46096), 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 46097 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.)

Assertion
Ref Expression
df-gte ≥ =

Detailed syntax breakdown of Definition df-gte
StepHypRef Expression
1 cge-real 46093 . 2 class
2 cle 10868 . . 3 class
32ccnv 5550 . 2 class
41, 3wceq 1543 1 wff ≥ =
Colors of variables: wff setvar class
This definition is referenced by:  gte-lte  46097  gte-lteh  46099
  Copyright terms: Public domain W3C validator