ax6_add_lt

Énoncé

∀ (a : ℝ) (b : ℝ) (c : ℝ), a < b → a + c < b + c

Ajouter un même nombre aux deux membres d’une inégalité la préserve.

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_add_lt

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

Code

axiom ax6_add_lt : ∀ a b c : ℝ,
  a < b → a + c < b + c