ax7_completude

Énoncé

∀ (A : ℝ → Prop), ∃ x, A x → ∃ b, estMajorant A b → ∃ s, estBorneSup A s

Toute partie non vide et majorée admet une borne supérieure. C’est cet axiome, et lui seul, qui distingue ℝ de ℚ.

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.

• ax7_completude

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

Code

axiom ax7_completude :
  ∀ A : ℝ → Prop,
  (∃ x, A x) →                -- A non vide
  (∃ b, estMajorant A b) →    -- A majoré
  ∃ s, estBorneSup A s        -- le sup existe dans ℝ

end

-- =============================================
-- AXIOMES 8-9 : LOGIQUE CLASSIQUE
-- =============================================