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

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

def Exercise_A_1_3 : Decidable (∀ (X Y : Prop), (X → Y) → (¬X → ¬Y) → (X ↔ Y))

Вправа A.1.3.

Equations

• Exercise_A_1_3 = sorry

def Exercise_A_1_4 : Decidable (∀ (X Y : Prop), (X → Y) → (¬Y → ¬X) → (X ↔ Y))

Вправа A.1.4.

Equations

• Exercise_A_1_4 = sorry

def Exercise_A_1_5 : Decidable (∀ (X Y Z : Prop), (X ↔ Y) → (Y ↔ Z) → [X, Y, Z].TFAE)

Вправа A.1.5.

Equations

• Exercise_A_1_5 = sorry

def Exercise_A_1_6 : Decidable (∀ (X Y Z : Prop), (X → Y) → (Y → Z) → (Z → X) → [X, Y, Z].TFAE)

Вправа A.1.6.

Equations

• Exercise_A_1_6 = sorry