From ac3d9de35485af6c77148812359abdd15a5c1f92 Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Wed, 22 Jan 2025 15:32:37 +0100 Subject: [PATCH] use French --- Math2001/01_Proofs_by_Calculation/04_Proving_Inequalities.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Math2001/01_Proofs_by_Calculation/04_Proving_Inequalities.lean b/Math2001/01_Proofs_by_Calculation/04_Proving_Inequalities.lean index 34312f6..d8cd6c9 100644 --- a/Math2001/01_Proofs_by_Calculation/04_Proving_Inequalities.lean +++ b/Math2001/01_Proofs_by_Calculation/04_Proving_Inequalities.lean @@ -27,7 +27,7 @@ example {r s : ℚ} (h1 : s + 3 ≥ r) (h2 : s + r ≤ 3) : r ≤ 3 := by done -- Example 1.4.3 --- Exercise: type out the whole proof printed in the text as a Lean proof. +-- Exercice : écrire l'ensemble de la preuve dans comme une preuve en Lean. example {x y : ℝ} (h1 : y ≤ x + 5) (h2 : x ≤ -2) : x + y < 2 := by sorry done