La bibliothèque

17 énoncés admis, 39 démontrés à partir d’eux, 32 dépendances. Aucune bibliothèque extérieure, aucune tactique : chaque preuve est un terme que le noyau de Lean 4 accepte. Cliquez un nœud pour voir son énoncé, son code et les axiomes qu’il consomme.

And.left

And.right

ax1_add_comm

a + b = b + a

ax1_mul_comm

a * b = b * a

ax2_distrib

a * (b + c) = a * b + a * c

ax3_add_assoc

a + b + c = a + (b + c)

ax3_mul_assoc

a * b * c = a * (b * c)

ax4_add_zero

a + 0 = a

ax4_mul_one

a * 1 = a

ax4_one_ne_zero

False

ax5_add_neg

a + -a = 0

ax5_mul_inv

a * a⁻¹ = 1

ax6_add_lt

a + c < b + c

ax6_lt_trans

a < c

ax6_mul_pos

0 < a * b

ax6_trichotomy

a < b ∧ ¬a = b ∧ ¬b < a ∨ ¬a < b ∧ a = b ∧ ¬b < a ∨ ¬a < b ∧ ¬a = b ∧ b < a

ax7_completude

∃ s, estBorneSup A s

ax8_tiers_exclu

p ∨ ¬p

ax9_ext_fonctionnelle

f = g

congr

f₁ a₁ = f₂ a₂

congrArg

f a₁ = f a₂

congrFun

f a = g a

DeZero.and_intro

a ∧ b

DeZero.and_left

DeZero.and_right

DeZero.congr_arg

f a = f b

DeZero.congr_fun

f a = g a

DeZero.eq_subst

motif b

DeZero.eq_symm

b = a

DeZero.eq_trans

a = c

DeZero.exists_elim

DeZero.exists_intro

∃ x, p x

DeZero.false_elim

DeZero.iff_intro

a ↔ b

DeZero.iff_mp

DeZero.iff_mpr

DeZero.or_elim

DeZero.or_inl

a ∨ b

DeZero.or_inr

a ∨ b

Eq.subst

motive b

Eq.symm

b = a

Eq.trans

a = c

Exists.elim

Iff.mp

Iff.mpr

Or.elim

add_right_cancel

a = b

cas_sur

DeZero.absurde

DeZero.congr_both

f a = g b

DeZero.ne_elim

le_trans

a ≤ c

par_absurde

zero_add

0 + a = a

neg_neg

- -a = a

non_non

admis logique démontré3 niveaux · les fils montent vers ce qui s’appuie dessus