ax4_one_ne_zero

Énoncé

1 = 0 → False

Un et zéro sont deux réels distincts. Sans cela, ℝ pourrait n’avoir qu’un élément.

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.

• ax4_one_ne_zero

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

Code

axiom ax4_one_ne_zero : (1 : ℝ) ≠ 0