new: Some more basic examples

LeanTalkSP24/basics2.lean

@@ -9,12 +9,37 @@ theorem sum_first_n {n : ℕ} : 2 * (range (n + 1)).sum id = n * (n + 1) := by
     linarith
 
 open Set
-variable {α : Type _}
-variable {s t u : Set α}
 
-example : s ∪ s ∩ t = s := by
+example {α : Type _} {s t : Set α} : s ∪ s ∩ t = s := by
   ext x; constructor
   rintro (xs | xsti)
   · trivial
   · exact And.left xsti
   exact Or.inl
+
+-- Examples of definitions
+def IsEven (n : ℕ) : Bool := (n%2) = 0
+def IsOdd (n : ℕ) : Bool := ¬IsEven n
+
+#eval IsEven 9
+#eval IsOdd 9
+
+example {n : ℕ} : IsOdd n = ((n%2) = 1) := by
+  apply iff_iff_eq.mp
+  constructor
+  -- <;>
+  · intro h
+    unfold IsOdd IsEven at h
+    simp at h
+    trivial
+  · intro h
+    unfold IsOdd IsEven
+    simp
+    trivial
+
+theorem nat_odd_or_even {n : ℕ} : (IsEven n)∨(IsOdd n):= by
+  apply or_iff_not_imp_left.mpr
+  intro h
+  unfold IsOdd
+  simp at *
+  trivial