ThmDex – An index of mathematical definitions, results, and conjectures.
▼ Set of symbols
▼ Alphabet
▼ Deduction system
▼ Theory
▼ Zermelo-Fraenkel set theory
▼ Set
▼ Binary cartesian set product
▼ Binary relation
▼ Binary endorelation
▼ Preordering relation
▼ Partial ordering relation
▼ Ordering relation
▼ Strict natural number ordering relation
▼ Strict integer ordering relation
▼ Strict rational ordering relation
▼ Strict real ordering relation
Definition D871
Basic real ordering relation
Results
▶ R4228: Real ordering is compatible with addition
Remarks
▶
Remark 0 (Proof technique: establishing a basic real equality by applying antisymmetry to basic real inequalities)
Let $x, y \in \mathbb{R}$ each be a [[[d,993]]] and let $\leq$ be the [[[d,871]]] on $\mathbb{R}$. If one was tasked to prove the equality $x = y$, then the following would be one potential approach. Result [[[r,3940]]] shows that $\leq$ is an [[[d,289]]] on $\mathbb{R}$. Thus, following the approach stated in its full generality in [[[k,657]]], to show the equality $x = y$, it is sufficient to show that $x \leq y$ and $y \leq x$.