From 07cdb8b35d19398b8d816ea8fc3165bdea4dd4a5 Mon Sep 17 00:00:00 2001 From: Lorenzo Luccioli Date: Wed, 18 Sep 2024 15:45:07 +0200 Subject: [PATCH] add Seminar_example.lean file --- Seminar_example.lean | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) create mode 100644 Seminar_example.lean diff --git a/Seminar_example.lean b/Seminar_example.lean new file mode 100644 index 00000000..f1f675b3 --- /dev/null +++ b/Seminar_example.lean @@ -0,0 +1,30 @@ +import Mathlib.Data.Real.Basic +import Mathlib.MeasureTheory.MeasurableSpace.Defs +import Mathlib.Tactic.Ring + +namespace Example + +def Measurable {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] + (f : α → β) : Prop := + ∀ (t : Set β), MeasurableSet t → MeasurableSet (f ⁻¹' t) + +theorem add_sub_cancel (a b : ℝ) : b + a - b = a := by + rw [add_comm] + rw [add_sub_assoc] + rw [sub_self] + exact add_zero a + +-- Example of a wrong proof +-- example (a b : ℝ) : b + a - b = a := by +-- exact add_zero a + +example (a b : ℝ) : b + a - b = a := by + rw [add_comm, add_sub_assoc, sub_self, add_zero] + +example (a b : ℝ) : b + a - b = a := by + ring + +example (a b : ℝ) (ha_pos : 0 < a) (hb_pos : 0 < b) : 0 < a + b := by + exact add_pos ha_pos hb_pos + +end Example