ax6_trichotomy

Énoncé

∀ (a : ℝ) (b : ℝ), a < b ∧ ¬a = b ∧ ¬b < a ∨ ¬a < b ∧ a = b ∧ ¬b < a ∨ ¬a < b ∧ ¬a = b ∧ b < a

De deux réels, ou bien l’un est plus petit, ou bien ils sont égaux, ou bien l’autre est plus petit — un cas et un seul.

Axiomes consommés

C’est un axiome : il est admis, pas démontré. Tout ce qui s’appuie dessus en hérite, et c’est précisément ce que cette bibliothèque rend visible.

• ax6_trichotomy

Vocabulaire admis : myLt, ℝ — les déclarations qui nomment ℝ et ses opérations, communes à toute la bibliothèque.

Code

axiom ax6_trichotomy : ∀ a b : ℝ,
  (a < b ∧ ¬ a = b ∧ ¬ b < a) ∨
  (¬ a < b ∧  a = b ∧ ¬ b < a) ∨
  (¬ a < b ∧ ¬ a = b ∧  b < a)
-- soit a est strictement inférieur à b
-- soit a est égal à b
-- soit b est strictement inférieur à a

-- Transitivité (axiome d'ordre manquant)