lean-talk-sp24/LeanTalkSP24/basics2.lean
2024-02-07 16:47:21 -06:00

46 lines
912 B
Text
Raw Permalink Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

import Mathlib.Tactic
open Finset
theorem sum_first_n {n : } : 2 * (range (n + 1)).sum id = n * (n + 1) := by
induction' n with d hd
· simp
· rw [sum_range_succ, mul_add, hd, id.def, Nat.succ_eq_add_one]
linarith
open Set
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
#eval IsEven 8
#eval IsOdd 8
example {n : } : IsOdd n ↔ ((n%2) = 1) := by
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