Аналіз I, Додаток A.2

Вступ до висновків. Демонструє деякі базові тактики та синтаксис Lean.

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

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

Теорема 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