ax6_mul_pos

Énoncé

∀ (a : ℝ) (b : ℝ), 0 < a → 0 < b → 0 < a * b

Le produit de deux nombres strictement positifs l’est aussi.

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_mul_pos

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

Code

axiom ax6_mul_pos : ∀ a b : ℝ,
  (0 : ℝ) < a → (0 : ℝ) < b → (0 : ℝ) < a * b

-- =============================================
-- AXIOME 7 : COMPLÉTUDE
-- =============================================

-- Un majorant de A est un élément au dessus de tout A