Analysis I, Appendix A.2: Implication

An introduction to implications. Showcases some basic tactics and Lean syntax.

theorem example_A_2_1 (x : ℤ) : x = 2 → x ^ 2 = 4

theorem theorem_A_2_4 (n : ℤ) : Even (n * (n + 1))

Theorem A.2.4

theorem contrapositive {X Y : Prop} (hXY : X → Y) : ¬Y → ¬X

theorem imp_example (x : ℝ) : x = 2 → x ^ 2 = 4

theorem imp_contrapositive (x : ℝ) : x ^ 2 ≠ 4 → x ≠ 2